Main results 1 to 100

Declaration Kind Where Note
CategoryTheory.isIso_id_sub_comp_iff theorem GeneralLinearGroups/RectangularIsomorphisms.lean, line 71 In a preadditive category with independent object and morphism universes, for arbitrary objects X, Y and morphisms a:X->Y, b:Y->X, IsIso (πŸ™ X - a ≫ b) iff IsIso (πŸ™ Y - b ≫ a). No finiteness, biproduct or nonzero-object hypothesis is imposed.
CategoryTheory.inv_id_sub_comp theorem GeneralLinearGroups/RectangularIsomorphisms.lean, line 85 Assuming only IsIso (πŸ™ Y - b ≫ a), the canonical inverse of πŸ™ X - a ≫ b is πŸ™ X + a ≫ inv (πŸ™ Y - b ≫ a) ≫ b. The left IsIso proof is derived from the criterion, not a second premise.
Matrix.list_prod_apply_mem_ideal_pow theorem GeneralLinearGroups/MatrixNilpotentIdeal.lean, line 62 Over a Semiring, an ordered list As of square matrices with entries in the same left ideal I has each product entry in I^As.length, for independently-universed finite decidable indices. Empty lists and indices are included. Right-append induction matches I^(k+1)=I^k*I; no commutativity, two-sidedness or monoid on left ideals is assumed.
Matrix.pow_apply_mem_ideal_pow theorem GeneralLinearGroups/MatrixNilpotentIdeal.lean, line 85 The replicate specialization gives entries of A^k in I^k for every natural k, including zero, over a Semiring with finite decidable indices.
Matrix.isNilpotent_of_isNilpotent_ideal theorem GeneralLinearGroups/MatrixNilpotentIdeal.lean, line 93 Uniform nilpotence of the left ideal containing all matrix entries implies matrix nilpotence, with the same vanishing exponent, even when that exponent is zero. No two-sidedness, Nonempty, commutativity, additive inverses or nontriviality premise is imposed; pointwise nilness of an ideal is not asserted to suffice.
Matrix.GeneralLinearGroup.StableGL abbrev GeneralLinearGroups/StableGeneralLinear.lean, line 193 Direct limit of finite GL groups under injective initial-segment stabilization over any Semiring, including the zero semiring and empty rank; finite representatives have an eventual equality criterion.
Matrix.GeneralLinearGroup.StableGL.map def GeneralLinearGroups/StableGeneralLinear.lean, line 265 Semiring-hom coefficient maps on stable GL commute with finite stages and respect identities and composition; compatible finite maps lift.
Matrix.GeneralLinearGroup.stableElementarySubgroup_eq_commutator theorem GeneralLinearGroups/StableElementary.lean, line 200 Over any Ring, the directed union of finite elementary images equals the commutator subgroup of stable GL. This does not assert same-rank ambient normality or commutator containment for finite GL.
Matrix.GeneralLinearGroup.stableElementarySubgroup_isPerfect instance GeneralLinearGroups/StableElementary.lean, line 256 The stable elementary subgroup is perfect as a group in its own right over any Ring, without a lower-rank restriction on stable GL.
Matrix.GeneralLinearGroup.stableElementaryAbelianizationEquiv def GeneralLinearGroups/StableElementary.lean, line 340 Over any Ring, the stable elementary quotient is an abelian group canonically equivalent to the abelianization; this equivalence is natural under ring-hom coefficient maps.
Matrix.GeneralLinearGroup.StableGL.rankOneUnits_injective theorem GeneralLinearGroups/StableDeterminant.lean, line 40 Rank-one units inject into stable GL over any Semiring, including noncommutative coefficients; their map is natural under semiring homs.
Matrix.GeneralLinearGroup.StableGL.quotientRankOneUnits_map theorem GeneralLinearGroups/StableDeterminant.lean, line 235 The rank-one map into the stable elementary quotient is natural over Rings; commutativity is needed only for its determinant retraction.
Matrix.GeneralLinearGroup.StableGL.abelianizationRankOneUnits_map theorem GeneralLinearGroups/StableDeterminant.lean, line 259 The rank-one map into the stable abelianization is natural over Semirings; commutativity is needed only for its determinant retraction.
Matrix.GeneralLinearGroup.StableGL.det def GeneralLinearGroups/StableDeterminant.lean, line 71 Compatible finite determinants define the stable determinant to units over any CommRing, including empty rank and the zero ring; it is natural under commutative-ring coefficient maps.
Matrix.GeneralLinearGroup.StableGL.det_comp_rankOneUnits theorem GeneralLinearGroups/StableDeterminant.lean, line 86 Over any CommRing, rank-one units give a right inverse to the stable determinant, hence the determinant is surjective.
Matrix.GeneralLinearGroup.StableGL.elementary_le_ker_det theorem GeneralLinearGroups/StableDeterminant.lean, line 113 Over any CommRing, stable elementary matrices lie in the determinant kernel; this is only an inclusion, not an equality.
Matrix.GeneralLinearGroup.StableGL.quotientDet_eq_abelianizationDet theorem GeneralLinearGroups/StableDeterminant.lean, line 192 Over any CommRing, determinant factorizations through the stable elementary quotient and the abelianization agree under their canonical equivalence; neither factorization identifies the kernel.
Matrix.GeneralLinearGroup.StableGL.quotientDet_quotientRankOneUnits theorem GeneralLinearGroups/StableDeterminant.lean, line 141 Over any CommRing, the ring-level quotient rank-one map is a section of the determinant induced on the stable elementary quotient.
Matrix.GeneralLinearGroup.StableGL.quotientDetKernelMulEquiv def GeneralLinearGroups/StableDeterminant.lean, line 267 Over any CommRing, including the zero ring, the abelian stable elementary quotient splits as its quotient determinant kernel times the units via the rank-one section. Its coordinate and coefficient-map laws do not identify or trivialize the kernel.
Matrix.GeneralLinearGroup.StableGL.abelianizationDet_abelianizationRankOneUnits theorem GeneralLinearGroups/StableDeterminant.lean, line 180 Over any CommRing, the semiring-level abelianization rank-one map is a section of the determinant induced on the abelianization.
Matrix.GeneralLinearGroup.elementaryUnit def GeneralLinearGroups/Elementary.lean, line 42 Off-diagonal unit 1 + single i j c over any Ring, with inverse, coefficient-addition product and a CommRing-only comparison with Mathlib transvections. It requires a finite decidable index type and i different from j, not a commutative coefficient ring.
Matrix.GeneralLinearGroup.elementarySubgroup def GeneralLinearGroups/Elementary.lean, line 74 Closure of elementary units, including generator and ordered-list product membership. It is bottom for subsingleton indices without implying that the entire GL group is trivial.
Matrix.GeneralLinearGroup.upperUnit_mem_elementarySubgroup theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 73 Upper block units lie in the elementary subgroup by single-entry decomposition, including empty indices and noncommutative rings.
Matrix.GeneralLinearGroup.lowerUnit_mem_elementarySubgroup theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 86 Lower block units use the negative lower-left block over any Ring.
Matrix.GeneralLinearGroup.blockDiagonalUnit_mem_elementarySubgroup theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 117 Doubled diag(g, g⁻¹) lies in the elementary subgroup using the signed swap membership and the existing ordered Whitehead factorization.
Matrix.GeneralLinearGroup.zeroProductUnit def GeneralLinearGroups/ZeroProductStabilization.lean, line 31 For independent finite index types and B * A = 0 over any Ring, constructs the unit 1 + A * B with inverse 1 - A * B.
Matrix.GeneralLinearGroup.zeroProductUnit_val theorem GeneralLinearGroups/ZeroProductStabilization.lean, line 41 Reads back the underlying matrix as 1 + A * B.
Matrix.GeneralLinearGroup.zeroProductUnit_inv_val theorem GeneralLinearGroups/ZeroProductStabilization.lean, line 47 Reads back the inverse matrix as 1 - A * B.
Matrix.GeneralLinearGroup.stabilize_zeroProductUnit_eq theorem GeneralLinearGroups/ZeroProductStabilization.lean, line 56 Stabilization of the zero-product unit equals the ordered commutator of rectangular upper and lower block shears, including empty blocks.
Matrix.GeneralLinearGroup.stabilize_zeroProductUnit_mem_elementarySubgroup theorem GeneralLinearGroups/ZeroProductStabilization.lean, line 70 The stabilized unit lies in the existing elementary subgroup over any Ring, including noncommutative and zero rings.
Matrix.GeneralLinearGroup.mapRingHom def GeneralLinearGroups/Whitehead.lean, line 31 Coefficient maps on finite general linear groups over arbitrary semirings.
Matrix.GeneralLinearGroup.blockDiagonalUnit_eq theorem GeneralLinearGroups/Whitehead.lean, line 115 Signed four-factor decomposition of diag(g, inverse g) over arbitrary rings.
Matrix.GeneralLinearGroup.mapRingHom_liftBlockDiagonal theorem GeneralLinearGroups/Whitehead.lean, line 183 A surjective ring homomorphism lifts this doubled block diagonal. It need not induce a surjection on the original finite GL.
Matrix.GeneralLinearGroup.reindexEquiv def GeneralLinearGroups/Reindex.lean, line 31 Equivalence along a finite-index-type equivalence, with identity, composition, inverse and coefficient-map laws; not stabilization between unequal cardinalities.
TwoSidedIdeal.isQuasiregular_iff_isRightQuasiregular theorem GeneralLinearGroups/QuasiregularIdeal.lean, line 119 The right-quasi-inverse condition is quantified over every element of the two-sided ideal. A single right inverse is not asserted to be two-sided in an arbitrary ring.
TwoSidedIdeal.ringJacobson_isGreatest_isQuasiregular theorem GeneralLinearGroups/QuasiregularIdeal.lean, line 207 The Jacobson radical is the greatest quasiregular two-sided ideal.
TwoSidedIdeal.IsNil.le_ringJacobson theorem GeneralLinearGroups/NilIdeal.lean, line 55 Pointwise nil ideals are quasiregular and contained in the Jacobson radical; no common exponent or nilpotence of the whole ideal is assumed.
TwoSidedIdeal.IsQuasiregular.matrix theorem GeneralLinearGroups/MatrixQuasiregular.lean, line 30 Entrywise finite matrix ideals preserve quasiregularity, including empty indices.
TwoSidedIdeal.quotientDivisionRing abbrev GeneralLinearGroups/LocalQuotient.lean, line 49 A proper two-sided ideal with unit complement gives a maximal left ideal and a division-ring quotient; commutativity and uniqueness of maximal ideals are not assumed.
Matrix.GeneralLinearGroup.idealGeneralLinearGroupEquivCongruence def GeneralLinearGroups/CongruenceSubgroup.lean, line 301 The ideal-unitization augmentation kernel is equivalent to the ambient congruence subgroup. Ambient injectivity and multiplicative exactness hold for every two-sided ideal, independently of quotient surjectivity.
RingHom.isQuasiregular_ker theorem GeneralLinearGroups/QuasiregularQuotient.lean, line 202 For R : Type u and S : Type v with Ring R and Semiring S, a map f : R β†’+* S with IsLocalHom f has quasi-regular canonical two-sided kernel TwoSidedIdeal.ker f, without surjectivity. The universes are independent; no commutativity, local-ring, nontriviality or nilness assumption is needed.
RingHom.isLocalHom_iff_isQuasiregular_ker theorem GeneralLinearGroups/QuasiregularQuotient.lean, line 214 For a surjective f : R β†’+* S from a possibly noncommutative Ring to a Semiring, IsLocalHom f is equivalent to quasi-regularity of the canonical two-sided kernel TwoSidedIdeal.ker f. Source and target universes are independent; no local-ring or nontriviality hypothesis is imposed. Surjectivity is essential for this equivalence: the inclusion of integers into rationals has zero kernel but fails to reflect units.
RingHom.isLocalHom_of_surjective_of_isQuasiregular_ker theorem GeneralLinearGroups/QuasiregularQuotient.lean, line 181 A surjective homomorphism from a possibly noncommutative Ring to a Semiring with quasi-regular canonical two-sided kernel gives Mathlib's IsLocalHom, with independent source and target universes and no commutativity, locality or nontriviality assumption. Existing APIs give unit reflection and surjectivity of the induced units map; nil kernels specialize through TwoSidedIdeal.IsNil.isQuasiregular.
Matrix.GeneralLinearGroup.isUnit_of_mapMatrix_quotient_isUnit theorem GeneralLinearGroups/QuasiregularQuotient.lean, line 77 A specified finite square matrix is a unit if its image modulo a quasiregular two-sided ideal is a unit; empty indices are allowed.
Matrix.GeneralLinearGroup.idealGeneralLinearGroupToRing_shortExact theorem GeneralLinearGroups/QuasiregularQuotient.lean, line 147 The three injective, multiplicatively exact and surjective assertions hold under quasiregularity. This is not arbitrary quotient GL surjectivity.
NonUnital.positivePow def GeneralLinearGroups/NonUnitalNilpotent.lean, line 41 positivePow x k multiplies k+1 copies, without a multiplicative identity; NonUnital.IsNilpotent asks for such a positive power to vanish.
Matrix.IsStrictlyUpperTriangular.isNilpotent theorem GeneralLinearGroups/NonUnitalNilpotent.lean, line 186 Strictly upper triangular Fin n matrices over nonunital rings are nilpotent. The uniform n+1-copy witness includes the empty matrix.
Matrix.GeneralLinearGroup.nilpotentMatrixElement def GeneralLinearGroups/NonUnitalNilpotent.lean, line 293 A vanishing power after entrywise unitization constructs a kernel element with value 1+x and an explicit finite alternating geometric inverse. The supplied exponent may be zero only when its power equation holds.
Matrix.GeneralLinearGroup.isUnit_one_add_unitizationMatrix_iff_isQuasiregular theorem GeneralLinearGroups/NonUnitalQuasiregular.lean, line 83 Nonunital quasiregularity is equivalent to invertibility of 1+x after unitization, and to representability in the augmentation kernel. No coefficient commutativity or nontriviality is inserted.
Unitization.ringEquivProd def GeneralLinearGroups/UnitalComparison.lean, line 36 A unital algebra's unitization is the product of its commutative scalar ring and the algebra; the coefficient algebra need not be commutative.
Matrix.GeneralLinearGroup.nonUnitalGeneralLinearGroupEquiv def GeneralLinearGroups/UnitalComparison.lean, line 135 For a unital ring, the augmentation-kernel group is the ordinary finite GL.
Ring.additiveCommutators def GeneralLinearGroups/AdditiveCommutator.lean, line 50 Additive-subgroup closure of ab-ba in a unital ring. It is not defined as a two-sided ideal.
Matrix.trace_mul_sub_trace_mul_commutators theorem GeneralLinearGroups/MatrixTrace.lean, line 55 A rectangular cyclic trace difference is a finite sum of scalar commutators, not generally zero in a noncommutative coefficient ring.
Matrix.traceOnCommutatorQuotient def GeneralLinearGroups/MatrixTrace.lean, line 85 Trace descends through the full additive commutator closure, even for empty indices.
Matrix.traceQuotientEquiv def GeneralLinearGroups/MatrixTrace.lean, line 191 For a chosen index p, trace is an additive equivalence with corner inverse r mapped to single p p r. Matrix-unit decomposition gives a membership criterion, inverse/representative laws and corner independence. No ring equivalence or empty-index inverse is asserted.
Matrix.GeneralLinearGroup.elementaryUnit_commute_disjoint theorem GeneralLinearGroups/ElementaryCommutator.lean, line 31 Elementary units commute when neither off-diagonal position composes with the other.
Matrix.GeneralLinearGroup.elementaryUnit_commutator theorem GeneralLinearGroups/ElementaryCommutator.lean, line 59 The ordered elementary commutator relation, valid for noncommutative rings.
Matrix.GeneralLinearGroup.elementaryUnit_eq_commutator theorem GeneralLinearGroups/ElementaryCommutator.lean, line 72 A third index expresses every elementary generator as a commutator of generators.
Matrix.GeneralLinearGroup.elementarySubgroup_isPerfect_of_three_le_card theorem GeneralLinearGroups/ElementaryCommutator.lean, line 80 The finite-rank elementary subgroup is perfect as soon as there are three indices.
Matrix.GeneralLinearGroup.mapRingHom_elementaryUnit theorem GeneralLinearGroups/RelativeElementary.lean, line 32 Entrywise coefficient mapping sends an elementary unit to an elementary unit.
Matrix.GeneralLinearGroup.mapRingHom_elementarySubgroup_le theorem GeneralLinearGroups/RelativeElementary.lean, line 41 Entrywise coefficient mapping preserves the absolute elementary subgroup.
Matrix.GeneralLinearGroup.mapElementarySubgroup def GeneralLinearGroups/RelativeElementary.lean, line 52 The restricted map on elementary subgroups.
Matrix.GeneralLinearGroup.mapElementarySubgroup_coe theorem GeneralLinearGroups/RelativeElementary.lean, line 60 The restricted coefficient map has the same ambient GL value as mapRingHom.
Matrix.GeneralLinearGroup.mapElementarySubgroup_elementaryUnit theorem GeneralLinearGroups/RelativeElementary.lean, line 65 The restricted coefficient map sends an elementary generator to its mapped-coefficient generator.
Matrix.GeneralLinearGroup.mapElementarySubgroup_id theorem GeneralLinearGroups/RelativeElementary.lean, line 76 Identity ring hom induces the identity restricted elementary map.
Matrix.GeneralLinearGroup.mapElementarySubgroup_comp theorem GeneralLinearGroups/RelativeElementary.lean, line 83 Composition of ring homs agrees with composition of restricted elementary maps.
Matrix.GeneralLinearGroup.relativeElementaryGenerators def GeneralLinearGroups/RelativeElementary.lean, line 91 Elementary generators with coefficients in I, viewed as members of E(R).
Matrix.GeneralLinearGroup.relativeElementarySubgroup def GeneralLinearGroups/RelativeElementary.lean, line 98 The normal closure of the ideal-coefficient generators inside E(R).
Matrix.GeneralLinearGroup.elementaryUnit_mem_relativeElementarySubgroup theorem GeneralLinearGroups/RelativeElementary.lean, line 103 Every ideal-coefficient elementary unit belongs to the relative subgroup.
Matrix.GeneralLinearGroup.relativeElementarySubgroup_normal instance GeneralLinearGroups/RelativeElementary.lean, line 109 The relative subgroup is normal inside the absolute elementary group.
Matrix.GeneralLinearGroup.relativeElementarySubgroup_mono theorem GeneralLinearGroups/RelativeElementary.lean, line 115 Enlarging the ideal enlarges its relative elementary subgroup.
Matrix.GeneralLinearGroup.relativeElementarySubgroup_bot theorem GeneralLinearGroups/RelativeElementary.lean, line 123 The zero ideal has trivial relative elementary subgroup, including in rank zero or one.
Matrix.GeneralLinearGroup.relativeElementarySubgroup_le_congruenceSubgroup theorem GeneralLinearGroups/RelativeElementary.lean, line 133 Relative elementary elements reduce to the identity modulo their ideal.
Matrix.GeneralLinearGroup.relativeElementarySubgroup_map_subtype_le_congruenceSubgroup theorem GeneralLinearGroups/RelativeElementary.lean, line 151 The image of the relative group in the ambient GL lies in the existing congruence kernel. This is an image inclusion, not a claim of ambient normality.
Matrix.GeneralLinearGroup.mapElementarySubgroup_relativeElementarySubgroup_le theorem GeneralLinearGroups/RelativeElementary.lean, line 161 Compatible coefficient maps carry relative elementary groups into relative elementary groups, without any surjectivity assumption.
Matrix.GeneralLinearGroup.upperUnit_zero theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 30 The upper block unit with zero off-diagonal block is the identity.
Matrix.GeneralLinearGroup.lowerUnit_zero theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 36 The lower block unit with zero off-diagonal block is the identity.
Matrix.GeneralLinearGroup.upperUnit_add theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 42 Upper block units turn matrix addition into group multiplication.
Matrix.GeneralLinearGroup.lowerUnit_add theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 48 Lower block units turn matrix addition into group multiplication.
Matrix.GeneralLinearGroup.upperUnit_single theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 54 A single upper-block entry is an off-block elementary unit.
Matrix.GeneralLinearGroup.lowerUnit_single theorem GeneralLinearGroups/ElementaryWhitehead.lean, line 63 A single lower-block entry is elementary with coefficient -c.
Matrix.GeneralLinearGroup.upperUnit_mem_relativeElementarySubgroup theorem GeneralLinearGroups/RelativeWhitehead.lean, line 32 An ideal-valued upper block unit belongs to the doubled relative elementary subgroup; this also holds for an empty index type.
Matrix.GeneralLinearGroup.lowerUnit_mem_relativeElementarySubgroup theorem GeneralLinearGroups/RelativeWhitehead.lean, line 71 An ideal-valued lower block unit belongs to the doubled relative elementary subgroup. Its lower-left block is -a, so its elementary generators use -a i j.
Matrix.GeneralLinearGroup.blockDiagonalUnit_eq_five theorem GeneralLinearGroups/RelativeWhitehead.lean, line 110 The five-factor block identity; lowerUnit b has lower-left block -b. No ideal hypothesis is needed.
Matrix.GeneralLinearGroup.blockDiagonalUnit_mem_relativeElementarySubgroup theorem GeneralLinearGroups/RelativeWhitehead.lean, line 137 The Whitehead diagonal of a congruence unit is relative elementary after doubling, with conjugation only inside the existing elementary subgroup.
Matrix.GeneralLinearGroup.stabilize def GeneralLinearGroups/ElementaryStabilization.lean, line 36 Extend an invertible matrix by an identity block, with no positivity assumption on the sizes of either block.
Matrix.GeneralLinearGroup.stabilize_apply_inl_inl theorem GeneralLinearGroups/ElementaryStabilization.lean, line 50 Stabilization agrees with the original unit on the upper-left block.
Matrix.GeneralLinearGroup.stabilize_apply_inl_inr theorem GeneralLinearGroups/ElementaryStabilization.lean, line 54 Stabilization has zero upper-right block.
Matrix.GeneralLinearGroup.stabilize_apply_inr_inl theorem GeneralLinearGroups/ElementaryStabilization.lean, line 58 Stabilization has zero lower-left block.
Matrix.GeneralLinearGroup.stabilize_apply_inr_inr theorem GeneralLinearGroups/ElementaryStabilization.lean, line 62 Stabilization has the identity lower-right block.
Matrix.GeneralLinearGroup.stabilize_injective theorem GeneralLinearGroups/ElementaryStabilization.lean, line 66 The original matrix can be recovered from the upper-left block.
Matrix.GeneralLinearGroup.mapRingHom_stabilize theorem GeneralLinearGroups/ElementaryStabilization.lean, line 80 Stabilization commutes with entrywise mapping of coefficients.
Matrix.GeneralLinearGroup.stabilize_elementaryUnit theorem GeneralLinearGroups/ElementaryStabilization.lean, line 97 Stabilization sends an elementary generator exactly to the corresponding generator on the first summand.
Matrix.GeneralLinearGroup.stabilize_elementarySubgroup_le theorem GeneralLinearGroups/ElementaryStabilization.lean, line 107 The image of the absolute elementary group under stabilization remains elementary.
Matrix.GeneralLinearGroup.stabilizeElementarySubgroup def GeneralLinearGroups/ElementaryStabilization.lean, line 121 Stabilization restricted to the existing elementary subgroups.
Matrix.GeneralLinearGroup.stabilizeElementarySubgroup_coe theorem GeneralLinearGroups/ElementaryStabilization.lean, line 129 Restricted stabilization has the same ambient value as the unit-group monoid hom.
Matrix.GeneralLinearGroup.stabilizeElementarySubgroup_elementaryUnit theorem GeneralLinearGroups/ElementaryStabilization.lean, line 134 Restricted stabilization evaluates on existing elementary generators.
Matrix.GeneralLinearGroup.stabilize_relativeElementarySubgroup_le theorem GeneralLinearGroups/ElementaryStabilization.lean, line 148 Relative elementary normal closures are preserved by stabilization as an image inclusion, without asserting surjectivity of the restricted map.
Matrix.GeneralLinearGroup.stabilize_congruenceSubgroup_le theorem GeneralLinearGroups/ElementaryStabilization.lean, line 162 Stabilization preserves the existing quotient-reduction congruence kernel.
Matrix.GeneralLinearGroup.stabilize_conj_eq_blockDiagonalUnit_conj theorem GeneralLinearGroups/RelativeWhiteheadConsequences.lean, line 31 Stabilized conjugation by g is conjugation by its elementary Whitehead diagonal, with no congruence assumption on g.

Quoted from the main results in formalization.yaml of FormalFrontier/general-linear-groups at commit a2199cf0, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.