SpecialLinearGroup

📁 Source: Mathlib/LinearAlgebra/SpecialLinearGroup.lean

Statistics

Metric	Count
Definitions toLin'_equiv, toLin_equiv, SpecialLinearGroup, baseChange, centerEquivRootsOfUnity, centerEquivRootsOfUnity_invFun, congr_linearEquiv, dualMap, instCoeFunForall, instDiv, instGroup, instInhabited, instInv, instMul, instOne, instPowInt, instPowNat, toGeneralLinearGroup, toLinearEquiv, «term_ᵀ»	20
Theorems symm_toLinearMap_eq, toLinearMap_eq, baseChange_apply_coe, centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, centerEquivRootsOfUnity_apply, centerEquivRootsOfUnity_apply_apply, centerEquivRootsOfUnity_apply_of_finrank_le_one, centerEquivRootsOfUnity_symm_apply, center_eq_bot_of_finrank_le_one, coe_div, coe_dualMap, coe_inv, coe_mk, coe_mul, coe_one, coe_pow, coe_toGeneralLinearGroup_apply, coe_zpow, congr_linearEquiv_apply_apply, congr_linearEquiv_coe_apply, congr_linearEquiv_refl, congr_linearEquiv_symm, congr_linearEquiv_trans, det_coe, det_eq_one, ext, ext_iff, mem_center_iff, mem_center_iff_spec, mem_range_toGeneralLinearGroup_iff, subsingleton_of_finrank_eq_one, toGeneralLinearGroup_injective, toGeneralLinearGroup_toLinearEquiv_apply, toLinearEquiv_apply, toLinearEquiv_injective, toLinearEquiv_symm_apply, toLinearEquiv_symm_to_linearMap, toLinearEquiv_to_linearMap, eq_one	39
Total	59

Matrix.SpecialLinearGroup

Definitions

Name	Category	Theorems
toLin'_equiv 📖	CompOp	—
toLin_equiv 📖	CompOp	3 math math: SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, toLin_equiv.symm_toLinearMap_eq, toLin_equiv.toLinearMap_eq

Matrix.SpecialLinearGroup.toLin_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm_toLinearMap_eq 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MulEquiv SpecialLinearGroup Matrix.SpecialLinearGroup SpecialLinearGroup.instMul Matrix.SpecialLinearGroup.hasMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm Matrix.SpecialLinearGroup.toLin_equiv LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype LinearEquiv.toLinearMap Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne	—	—
toLinearMap_eq 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne MulEquiv Matrix.SpecialLinearGroup SpecialLinearGroup Matrix.SpecialLinearGroup.hasMul SpecialLinearGroup.instMul EquivLike.toFunLike MulEquiv.instEquivLike Matrix.SpecialLinearGroup.toLin_equiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Matrix.module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFinsupp.instEquivLikeLinearEquiv Matrix.toLin Finite.of_fintype Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—

SpecialLinearGroup

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	1 math math: baseChange_apply_coe
centerEquivRootsOfUnity 📖	CompOp	5 math math: centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, centerEquivRootsOfUnity_symm_apply, centerEquivRootsOfUnity_apply, centerEquivRootsOfUnity_apply_apply, centerEquivRootsOfUnity_apply_of_finrank_le_one
centerEquivRootsOfUnity_invFun 📖	CompOp	—
congr_linearEquiv 📖	CompOp	4 math math: congr_linearEquiv_symm, congr_linearEquiv_coe_apply, congr_linearEquiv_refl, congr_linearEquiv_trans
dualMap 📖	CompOp	1 math math: coe_dualMap
instCoeFunForall 📖	CompOp	—
instDiv 📖	CompOp	1 math math: coe_div
instGroup 📖	CompOp	17 math math: toLinearEquiv_symm_to_linearMap, mem_center_iff, mem_range_toGeneralLinearGroup_iff, centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, centerEquivRootsOfUnity_symm_apply, centerEquivRootsOfUnity_apply, toLinearEquiv_symm_apply, center_eq_bot_of_finrank_le_one, toGeneralLinearGroup_injective, toGeneralLinearGroup_toLinearEquiv_apply, coe_toGeneralLinearGroup_apply, centerEquivRootsOfUnity_apply_apply, baseChange_apply_coe, toLinearEquiv_injective, toLinearEquiv_to_linearMap, centerEquivRootsOfUnity_apply_of_finrank_le_one, toLinearEquiv_apply
instInhabited 📖	CompOp	—
instInv 📖	CompOp	2 math math: toLinearEquiv_symm_to_linearMap, coe_inv
instMul 📖	CompOp	7 math math: congr_linearEquiv_symm, congr_linearEquiv_coe_apply, coe_mul, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, congr_linearEquiv_refl, congr_linearEquiv_trans
instOne 📖	CompOp	1 math math: coe_one
instPowInt 📖	CompOp	1 math math: coe_zpow
instPowNat 📖	CompOp	1 math math: coe_pow
toGeneralLinearGroup 📖	CompOp	4 math math: mem_range_toGeneralLinearGroup_iff, toGeneralLinearGroup_injective, toGeneralLinearGroup_toLinearEquiv_apply, coe_toGeneralLinearGroup_apply
toLinearEquiv 📖	CompOp	7 math math: toLinearEquiv_symm_to_linearMap, toLinearEquiv_symm_apply, toGeneralLinearGroup_toLinearEquiv_apply, coe_toGeneralLinearGroup_apply, toLinearEquiv_injective, toLinearEquiv_to_linearMap, toLinearEquiv_apply
«term_ᵀ» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_apply_coe 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup Algebra.to_smulCommClass instGroup baseChange LinearEquiv.baseChange	—	RingHomInvPair.ids Algebra.to_smulCommClass
centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq 📖	mathematical	—	Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe MulEquiv Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.instGroup Subgroup.center Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.trans SpecialLinearGroup instGroup Subgroup.centerCongr Matrix.SpecialLinearGroup.toLin_equiv centerEquivRootsOfUnity Fintype.card Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton rootsOfUnity.eq_one Module.finrank_eq_zero_iff_of_free commRing_strongRankCondition Nat.instZeroLEOneClass Module.finrank_eq_card_basis Fintype.card_of_isEmpty Module.Free.instFaithfulSMulOfNontrivial not_subsingleton_iff_nontrivial smulCommClass_self Subgroup.centerCongr_apply_coe LinearMap.ext centerEquivRootsOfUnity_apply_apply LinearEquiv.coe_toLinearMap LinearMap.ext_iff RingHomInvPair.ids Finite.of_fintype Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity Matrix.toLin_scalar FaithfulSMul.eq_of_smul_eq_smul MulEquiv.trans_apply
centerEquivRootsOfUnity_apply 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup rootsOfUnity Module.finrank LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul Subgroup.toGroup AddCommMonoid.toAddMonoid Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring CommRing.toRing Subgroup.smulCommClass_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toMulAction Units.smulCommClass_right smulCommClass_self MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike centerEquivRootsOfUnity LinearMap.id	—	Subgroup.smulCommClass_right Units.smulCommClass_right smulCommClass_self subsingleton_or_nontrivial dite_smul one_smul Module.subsingleton Subsingleton.eq_one Unique.instSubsingleton mem_center_iff Subtype.prop
centerEquivRootsOfUnity_apply_apply 📖	mathematical	—	Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring CommRing.toRing DFunLike.coe MulEquiv SpecialLinearGroup instGroup Subgroup.center Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike centerEquivRootsOfUnity	—	LinearEquiv.coe_toLinearMap Subgroup.smulCommClass_right Units.smulCommClass_right smulCommClass_self centerEquivRootsOfUnity_apply
centerEquivRootsOfUnity_apply_of_finrank_le_one 📖	mathematical	Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	DFunLike.coe MulEquiv SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center Units CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup rootsOfUnity Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike centerEquivRootsOfUnity Subgroup.one	—	SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass OneMemClass.coe_one rootsOfUnity.eq_one
centerEquivRootsOfUnity_symm_apply 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center MulEquiv CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup rootsOfUnity Module.finrank Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm centerEquivRootsOfUnity LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul Subgroup.toGroup AddCommMonoid.toAddMonoid Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring CommRing.toRing Subgroup.smulCommClass_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toMulAction Units.smulCommClass_right smulCommClass_self LinearMap.id	—	Subgroup.smulCommClass_right Units.smulCommClass_right smulCommClass_self LinearMap.coe_equivOfIsUnitDet
center_eq_bot_of_finrank_le_one 📖	mathematical	Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Subgroup.center SpecialLinearGroup instGroup Bot.bot Subgroup Subgroup.instBot	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton instSubsingletonSubtype_mathlib Finite.card_le_one_iff_subsingleton Finite.of_fintype Nat.card_eq_fintype_card Module.finrank_eq_card_basis commRing_strongRankCondition Matrix.SpecialLinearGroup.subsingleton_of_subsingleton Subgroup.eq_bot_of_subsingleton Equiv.subsingleton_congr
coe_div 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instDiv DivInvMonoid.toDiv	—	—
coe_dualMap 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing Semiring.toModule LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.id Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne dualMap LinearEquiv.dualMap	—	Algebra.to_smulCommClass
coe_inv 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instInv RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
coe_mk 📖	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne	—	—	RingHomInvPair.ids
coe_mul 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instMul MulOne.toMul	—	—
coe_one 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instOne RingHomInvPair.ids InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
coe_pow 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instPowNat Monoid.toNatPow	—	—
coe_toGeneralLinearGroup_apply 📖	mathematical	—	Units.val LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMonoid DFunLike.coe MonoidHom SpecialLinearGroup LinearMap.GeneralLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup Units.instMulOneClass MonoidHom.instFunLike toGeneralLinearGroup LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv LinearEquiv.automorphismGroup toLinearEquiv	—	—
coe_zpow 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SpecialLinearGroup instPowInt DivInvMonoid.toZPow	—	—
congr_linearEquiv_apply_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm	—	RingHomInvPair.ids
congr_linearEquiv_coe_apply 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne MulEquiv SpecialLinearGroup instMul EquivLike.toFunLike MulEquiv.instEquivLike congr_linearEquiv LinearEquiv.trans RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.symm	—	RingHomInvPair.ids
congr_linearEquiv_refl 📖	mathematical	—	congr_linearEquiv LinearEquiv.refl CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid MulEquiv.refl SpecialLinearGroup instMul	—	—
congr_linearEquiv_symm 📖	mathematical	—	MulEquiv.symm SpecialLinearGroup instMul congr_linearEquiv LinearEquiv.symm CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
congr_linearEquiv_trans 📖	mathematical	—	MulEquiv.trans SpecialLinearGroup instMul congr_linearEquiv LinearEquiv.trans CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids	—	RingHomInvPair.ids
det_coe 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne	—	Subtype.prop
det_eq_one 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap LinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass LinearEquiv.det Units.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids Subtype.prop
ext 📖	—	—	—	—	ext_iff
ext_iff 📖	—	—	—	—	—
mem_center_iff 📖	mathematical	—	SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.finrank AddCommGroup.toAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearEquiv Units DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring LinearMap.id	—	smulCommClass_self subsingleton_or_nontrivial instSubsingletonSubtype_mathlib Unique.instSubsingleton Subsingleton.eq_one SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Module.finrank_subsingleton pow_one RingHomInvPair.ids one_smul Module.finrank_eq_card_basis commRing_strongRankCondition MulEquivClass.apply_mem_center_iff MulEquiv.instMulEquivClass Matrix.SpecialLinearGroup.mem_center_iff Matrix.ext LinearMap.toMatrix_apply Finite.of_fintype LinearEquiv.injective NeZero.one map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Pi.single_apply mul_ite mul_one MulZeroClass.mul_zero
mem_center_iff_spec 📖	mathematical	SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearEquiv.toLinearMap LinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det Units.instOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Monoid.toNatPow Module.finrank AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing LinearMap.instSMul AddCommMonoid.toAddMonoid smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring LinearMap.id mem_center_iff	—	smulCommClass_self mem_center_iff LinearMap.ext_iff
mem_range_toGeneralLinearGroup_iff 📖	mathematical	—	LinearMap.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Set.instMembership Set.range SpecialLinearGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup Units.instMulOneClass LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid MonoidHom.instFunLike toGeneralLinearGroup LinearEquiv RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv.automorphismGroup LinearEquiv.det LinearMap.GeneralLinearGroup.toLinearEquiv Units.instOne	—	RingHomInvPair.ids toGeneralLinearGroup_toLinearEquiv_apply Subtype.prop
subsingleton_of_finrank_eq_one 📖	mathematical	Module.finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	SpecialLinearGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim instSubsingletonSubtype_mathlib Unique.instSubsingleton ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.ext RingHomInvPair.ids smulCommClass_self commRing_strongRankCondition Subtype.prop LinearEquiv.eq_symm_apply LinearMap.det_smul pow_one LinearMap.det_id mul_one LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one one_smul
toGeneralLinearGroup_injective 📖	mathematical	—	SpecialLinearGroup LinearMap.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup Units.instMulOneClass LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid MonoidHom.instFunLike toGeneralLinearGroup	—	EquivLike.toEmbeddingLike
toGeneralLinearGroup_toLinearEquiv_apply 📖	mathematical	—	LinearMap.GeneralLinearGroup.toLinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe MonoidHom SpecialLinearGroup LinearMap.GeneralLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup Units.instMulOneClass LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid MonoidHom.instFunLike toGeneralLinearGroup LinearEquiv RingHomInvPair.ids LinearEquiv.automorphismGroup toLinearEquiv	—	RingHomInvPair.ids
toLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MonoidHom SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup LinearEquiv.automorphismGroup MonoidHom.instFunLike toLinearEquiv	—	RingHomInvPair.ids
toLinearEquiv_injective 📖	mathematical	—	SpecialLinearGroup LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup LinearEquiv.automorphismGroup MonoidHom.instFunLike toLinearEquiv	—	Subtype.val_injective RingHomInvPair.ids
toLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm MonoidHom SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup LinearEquiv.automorphismGroup MonoidHom.instFunLike toLinearEquiv	—	RingHomInvPair.ids
toLinearEquiv_symm_to_linearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid LinearEquiv.symm DFunLike.coe MonoidHom SpecialLinearGroup LinearEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup LinearEquiv.automorphismGroup MonoidHom.instFunLike toLinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.instMulOneClass LinearEquiv.det Units.instOne instInv	—	RingHomInvPair.ids
toLinearEquiv_to_linearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid DFunLike.coe MonoidHom SpecialLinearGroup LinearEquiv MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup LinearEquiv.automorphismGroup MonoidHom.instFunLike toLinearEquiv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.instMulOneClass LinearEquiv.det Units.instOne	—	RingHomInvPair.ids

(root)

Definitions

Name	Category	Theorems
SpecialLinearGroup 📖	CompOp	30 math math: SpecialLinearGroup.coe_zpow, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, SpecialLinearGroup.mem_center_iff, SpecialLinearGroup.coe_one, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, SpecialLinearGroup.coe_inv, SpecialLinearGroup.congr_linearEquiv_symm, SpecialLinearGroup.congr_linearEquiv_coe_apply, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, SpecialLinearGroup.coe_mul, SpecialLinearGroup.coe_pow, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, SpecialLinearGroup.centerEquivRootsOfUnity_apply, SpecialLinearGroup.toLinearEquiv_symm_apply, SpecialLinearGroup.center_eq_bot_of_finrank_le_one, SpecialLinearGroup.toGeneralLinearGroup_injective, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, SpecialLinearGroup.congr_linearEquiv_refl, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, SpecialLinearGroup.baseChange_apply_coe, SpecialLinearGroup.coe_div, SpecialLinearGroup.congr_linearEquiv_trans, SpecialLinearGroup.toLinearEquiv_injective, SpecialLinearGroup.subsingleton_of_finrank_eq_one, SpecialLinearGroup.toLinearEquiv_to_linearMap, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, SpecialLinearGroup.toLinearEquiv_apply

rootsOfUnity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one 📖	mathematical	—	Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Units.instOne	—	Subtype.prop pow_one

---

← Back to Index