Main results 201 to 221

Declaration	Kind	Where	Note
Matrix.DualNumberMixedSLCommutator.mixedSLKernel	def	GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 108
Matrix.DualNumberMixedSLCommutator.mixedSLKernel_val	theorem	GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 113
Matrix.DualNumberMixedSLCommutator.mixedSLKernel_readback	theorem	GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 119
Matrix.DualNumberMixedSLCommutator.mixedSLKernel_snd_snd	theorem	GeneralLinearGroups/DualNumberMixedSLCommutator.lean, line 126
Matrix.GeneralLinearGroup.reindexEquiv_mem_elementarySubgroup	theorem	GeneralLinearGroups/UnitPivotDiagonalization.lean, line 41	Ring-level reindexing of the existing elementary subgroup.
Matrix.leadingPrincipalMinor	def	GeneralLinearGroups/UnitPivotDiagonalization.lean, line 162	Ordered Fin.castLE minor, including the empty minor.
Matrix.exists_elementary_diagonalization_of_unit_leadingPrincipalMinors	theorem	GeneralLinearGroups/UnitPivotDiagonalization.lean, line 424	Two-sided elementary reduction under all positive unit leading minors over a CommRing.
Matrix.exists_elementary_diagonalization_of_unit_pivot	theorem	GeneralLinearGroups/UnitPivotDiagonalization.lean, line 311	A unit first pivot lifts an elementary factorization of its Schur residual.
Matrix.GeneralLinearGroup.exists_elementary_diagonalization_local	theorem	GeneralLinearGroups/LocalElementaryGeneration.lean, line 92	Invertible matrices over commutative local rings reduce to a unit diagonal without a minor condition, including in rank zero.
Matrix.GeneralLinearGroup.mem_elementarySubgroup_iff_det_eq_one_local	theorem	GeneralLinearGroups/LocalElementaryGeneration.lean, line 106	Finite elementary membership is equivalent to determinant one on any finite decidable index type.
Matrix.GeneralLinearGroup.StableGL.elementary_eq_ker_det_local	theorem	GeneralLinearGroups/LocalElementaryGeneration.lean, line 130	The stable elementary subgroup is the stable determinant kernel over commutative local rings.
Matrix.GeneralLinearGroup.StableGL.quotientDet_ker_eq_bot_local	theorem	GeneralLinearGroups/LocalElementaryGeneration.lean, line 141	The existing quotient determinant has trivial kernel under the local-ring hypothesis.
Matrix.GeneralLinearGroup.StableGL.quotientDetMulEquiv	def	GeneralLinearGroups/LocalElementaryGeneration.lean, line 154	The existing quotient determinant and rank-one section form a natural multiplicative equivalence with coefficient units over local rings.
Matrix.GeneralLinearGroup.exists_elementary_transvection_diagonalization_field	theorem	GeneralLinearGroups/LocalElementaryGeneration.lean, line 226	Mathlib transvection lists yield elementary GL factors and a unit diagonal for invertible field matrices.
Matrix.GeneralLinearGroup.elementaryUnitPathSubtype	def	GeneralLinearGroups/ElementaryPaths.lean, line 74	Path within the elementary subgroup over a topological Ring.
Matrix.GeneralLinearGroup.elementarySubgroup_pathConnectedSpace	theorem	GeneralLinearGroups/ElementaryPaths.lean, line 85	Subgroup path-connectedness additionally requiring PathConnectedSpace R.
Matrix.GeneralLinearGroup.diagonalUnit_mem_elementarySubgroup	theorem	GeneralLinearGroups/ElementaryDiagonal.lean, line 186	Product-one unit diagonal membership over a CommRing, including empty indices.
Matrix.GeneralLinearGroup.mem_elementarySubgroup_of_det_one_of_unit_leadingPrincipalMinors	theorem	GeneralLinearGroups/ElementaryDiagonal.lean, line 252	Determinant-one membership requiring separately all positive unit leading minors.
Matrix.SpecialLinearGroup.elementarySubgroup	def	GeneralLinearGroups/ElementaryNeighborhood.lean, line 37	SL comap of the existing GL elementary subgroup, not the GL subgroup itself.
Matrix.SpecialLinearGroup.isOpen_elementarySubgroup	theorem	GeneralLinearGroups/ElementaryNeighborhood.lean, line 87	Openness requiring an open scalar unit locus, not coefficient path-connectedness.
Matrix.SpecialLinearGroup.elementarySubgroup_eq_pathComponentOne	theorem	GeneralLinearGroups/ElementaryNeighborhood.lean, line 122	Identity path-component equality requiring both open scalar units and PathConnectedSpace R.

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.