Basic

📁 Source: Mathlib/LinearAlgebra/GeneralLinearGroup/Basic.lean

Statistics

Metric	Count
Definitions congrLinearEquiv, generalLinearEquiv, ofLinearEquiv, toLinearEquiv	4
Theorems coeFn_generalLinearEquiv, coe_ofLinearEquiv, coe_toLinearEquiv, congrLinearEquiv_apply, congrLinearEquiv_refl, congrLinearEquiv_symm, congrLinearEquiv_trans, congrLinearEquiv_trans', generalLinearEquiv_to_linearMap, ofLinearEquiv_inv, ofLinearEquiv_mul, toLinearEquiv_inv, toLinearEquiv_mul	13
Total	17

LinearMap.GeneralLinearGroup

Definitions

Name	Category	Theorems
congrLinearEquiv 📖	CompOp	5 math math: congrLinearEquiv_refl, congrLinearEquiv_apply, congrLinearEquiv_symm, congrLinearEquiv_trans', congrLinearEquiv_trans
generalLinearEquiv 📖	CompOp	5 math math: generalLinearEquiv_to_linearMap, ModularGroup.lcRow0Extend_symm_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, ModularGroup.lcRow0Extend_apply, coeFn_generalLinearEquiv
ofLinearEquiv 📖	CompOp	4 math math: ofLinearEquiv_inv, congrLinearEquiv_apply, coe_ofLinearEquiv, ofLinearEquiv_mul
toLinearEquiv 📖	CompOp	8 math math: SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, toLinearEquiv_inv, Matrix.GeneralLinearGroup.toLin'_apply, congrLinearEquiv_apply, coe_toLinearEquiv, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, toLinearEquiv_mul, Projectivization.generalLinearGroup_smul_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_generalLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike MulEquiv LinearMap.GeneralLinearGroup Units.instMul LinearMap Module.End.instMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MulEquiv.instEquivLike generalLinearEquiv LinearMap.instFunLike Units.val	—	RingHomInvPair.ids
coe_ofLinearEquiv 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Units.val Module.End.instMonoid ofLinearEquiv LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike	—	RingHomInvPair.ids
coe_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv LinearMap LinearMap.instFunLike Units.val Module.End.instMonoid	—	RingHomInvPair.ids
congrLinearEquiv_apply 📖	mathematical	—	DFunLike.coe MulEquiv LinearMap.GeneralLinearGroup Units.instMul LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid EquivLike.toFunLike MulEquiv.instEquivLike congrLinearEquiv ofLinearEquiv LinearEquiv.trans RingHomInvPair.triples₂ RingHomInvPair.ids LinearEquiv.symm RingHomCompTriple.ids RingHomCompTriple.right_ids toLinearEquiv	—	—
congrLinearEquiv_refl 📖	mathematical	—	congrLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.refl MulEquiv.refl LinearMap.GeneralLinearGroup Units.instMul LinearMap Module.End.instMonoid	—	RingHomInvPair.ids
congrLinearEquiv_symm 📖	mathematical	—	MulEquiv.symm LinearMap.GeneralLinearGroup Units.instMul LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid congrLinearEquiv LinearEquiv.symm	—	—
congrLinearEquiv_trans 📖	mathematical	—	MulEquiv.trans LinearMap.GeneralLinearGroup Units.instMul LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid congrLinearEquiv RingHomInvPair.ids LinearEquiv.trans RingHomCompTriple.ids	—	RingHomInvPair.ids
congrLinearEquiv_trans' 📖	mathematical	—	MulEquiv.trans LinearMap.GeneralLinearGroup Units.instMul LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid congrLinearEquiv LinearEquiv.trans	—	—
generalLinearEquiv_to_linearMap 📖	mathematical	—	LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFunLike.coe MulEquiv LinearMap.GeneralLinearGroup LinearEquiv Units.instMul LinearMap Module.End.instMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup EquivLike.toFunLike MulEquiv.instEquivLike generalLinearEquiv Units.val	—	LinearMap.ext RingHomInvPair.ids
ofLinearEquiv_inv 📖	mathematical	—	ofLinearEquiv LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearEquiv.automorphismGroup LinearMap.GeneralLinearGroup Units.instInv LinearMap Module.End.instMonoid	—	RingHomInvPair.ids
ofLinearEquiv_mul 📖	mathematical	—	ofLinearEquiv LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup LinearMap.GeneralLinearGroup Units.instMul LinearMap Module.End.instMonoid	—	RingHomInvPair.ids
toLinearEquiv_inv 📖	mathematical	—	toLinearEquiv LinearMap.GeneralLinearGroup Units.instInv LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid LinearEquiv RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearEquiv.automorphismGroup	—	RingHomInvPair.ids
toLinearEquiv_mul 📖	mathematical	—	toLinearEquiv LinearMap.GeneralLinearGroup Units.instMul LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid LinearEquiv RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup	—	RingHomInvPair.ids

---

← Back to Index