Defs

📁 Source: Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

Statistics

Metric	Count
Definitions GLPos, det, instCoeFun, kronecker, map, mk', mk'', mkOfDetNeZero, scalar, toLin, toLin', hasCoeToGeneralLinearGroup, instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos, mapGL, toGL, toGLPos, instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos, instNegSubtypeGeneralLinearGroupMemSubgroupGLPos, termGL, «termGL(_,_)⁺»⁺»)	20
Theorems coe_neg, coe_neg_GL, coe_neg_apply, det_ne_zero, coe_inv, coe_map_inv_mul_map, coe_map_mul_map_inv, coe_mul, coe_one, coe_toLin, det_ne_zero, det_scalar, ext, ext_iff, map_apply, map_comp, map_comp_apply, map_det, map_id, map_inv, map_inv_mul_map, map_mul, map_mul_map_inv, map_one, toLin'_apply, toLin_apply, val_det_apply, val_inv_det_apply, val_inv_scalar_apply, val_map_apply, val_mk', val_mk'', val_mkOfDetNeZero, val_scalar_apply, kronecker, coeToGL_det, coe_GLPos_coe_GL_coe_matrix, coe_GLPos_neg, coe_GL_coe_matrix, coe_to_GLPos_to_GL_det, det_mapGL, mapGL_coe_matrix, mapGL_inj, mapGL_injective, map_mapGL, toGLPos_injective, toGL_inj, toGL_injective, mem_glpos	49
Total	69

Matrix

Definitions

Name	Category	Theorems
GLPos 📖	CompOp	14 math math: ModularGroup.SLOnGLPos_smul_apply, GLPos.coe_neg_apply, SpecialLinearGroup.toGLPos_injective, ModularGroup.coe_apply_complex, ModularGroup.SL_to_GL_tower, SpecialLinearGroup.coe_GLPos_neg, SpecialLinearGroup.coe_to_GLPos_to_GL_det, mem_glpos, ModularGroup.coe_one, SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, ModularGroup.det_coe, GLPos.coe_neg_GL, ModularGroup.coeHom_apply, GLPos.coe_neg
instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos 📖	CompOp	—
instNegSubtypeGeneralLinearGroupMemSubgroupGLPos 📖	CompOp	4 math math: GLPos.coe_neg_apply, SpecialLinearGroup.coe_GLPos_neg, GLPos.coe_neg_GL, GLPos.coe_neg
termGL 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_glpos 📖	mathematical	—	GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring SetLike.instMembership Subgroup.instSetLike GLPos Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike GeneralLinearGroup.det	—	—

Matrix.GLPos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_neg 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—
coe_neg_GL 📖	mathematical	—	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
coe_neg_apply 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—
det_ne_zero 📖	—	—	—	—	ne_of_gt Subtype.prop

Matrix.GeneralLinearGroup

Definitions

Name	Category	Theorems
det 📖	CompOp	25 math math: det_scalar, map_det, ModularForm.mul_slash, Matrix.SpecialLinearGroup.coeToGL_det, UpperHalfPlane.im_smul_eq_div_normSq, UpperHalfPlane.moebius_im, ModularForm.prod_slash, ModularForm.prod_slash_sum_weights, continuous_det, Subgroup.HasDetOne.det_eq, Matrix.SpecialLinearGroup.range_toGL, Subgroup.HasDetPlusMinusOne.det_eq, val_inv_det_apply, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, Matrix.mem_glpos, UpperHalfPlane.det_J, ModularForm.prod_fintype_slash, ModularForm.slash_def, Matrix.SpecialLinearGroup.det_mapGL, Subgroup.HasDetPlusMinusOne.abs_det, UpperHalfPlane.smulAux'_im, Subgroup.hasDetPlusMinusOne_iff_abs_det, ModularForm.slash_apply, val_det_apply, UpperHalfPlane.petersson_slash
instCoeFun 📖	CompOp	—
kronecker 📖	CompOp	—
map 📖	CompOp	20 math math: Matrix.SpecialLinearGroup.map_mapGL, map_det, map_comp_apply, CongruenceSubgroup.exists_Gamma_le_conj', map_inv_mul_map, OnePoint.map_smul, CongruenceSubgroup.IsArithmetic.conj, map_comp, map_inv, CongruenceSubgroup.isArithmetic_conj_SL2Z, CongruenceSubgroup.finiteIndex_conjGL, map_swap, map_mul_map_inv, val_map_apply, map_apply, map_one, map_mul, map_id, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, Subgroup.IsArithmetic.conj
mk' 📖	CompOp	1 math math: val_mk'
mk'' 📖	CompOp	1 math math: val_mk''
mkOfDetNeZero 📖	CompOp	1 math math: val_mkOfDetNeZero
scalar 📖	CompOp	5 math math: det_scalar, center_eq_range_scalar, center_eq_range_units, val_inv_scalar_apply, val_scalar_apply
toLin 📖	CompOp	4 math math: coe_toLin, ModularGroup.lcRow0Extend_symm_apply, ModularGroup.lcRow0Extend_apply, toLin_apply
toLin' 📖	CompOp	1 math math: toLin'_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inv 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Units.instInv Matrix.inv	—	Matrix.invOf_eq_nonsing_inv
coe_map_inv_mul_map 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.map Matrix.inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Matrix.nonsing_inv_mul Matrix.map_one map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
coe_map_mul_map_inv 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.map Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Matrix.inv Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Matrix.mul_nonsing_inv Matrix.map_one map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
coe_mul 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Units.instMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	—
coe_one 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Units.instOne Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
coe_toLin 📖	mathematical	—	Units.val LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule Module.End.instMonoid DFunLike.coe MulEquiv Matrix.GeneralLinearGroup LinearMap.GeneralLinearGroup Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring EquivLike.toFunLike MulEquiv.instEquivLike toLin Matrix.mulVecLin	—	—
det_ne_zero 📖	—	—	—	—	Units.ne_zero
det_scalar 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike det scalar Monoid.toNatPow Units.instMonoid Fintype.card	—	Units.ext Matrix.det_diagonal Finset.prod_const
ext 📖	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—	Units.ext Matrix.ext
ext_iff 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	Units.ext_iff Matrix.ext_iff
map_apply 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—
map_comp 📖	mathematical	—	map RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.comp Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	—
map_comp_apply 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike MonoidHom.comp map	—	—
map_det 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike det map Units.map MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring Monoid.toMulOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	—	Units.ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.map_det
map_id 📖	mathematical	—	map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.id Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	—
map_inv 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike map Units.instInv	—	map_inv MonoidHom.instMonoidHomClass
map_inv_mul_map 📖	mathematical	—	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike map Units.instInv Units.instOne	—	map_inv MonoidHom.instMonoidHomClass inv_mul_cancel
map_mul 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike map Units.instMul	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
map_mul_map_inv 📖	mathematical	—	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike map Units.instInv Units.instOne	—	map_inv MonoidHom.instMonoidHomClass mul_inv_cancel
map_one 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike map Units.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
toLin'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.GeneralLinearGroup.toLinearEquiv MulEquiv Matrix.GeneralLinearGroup LinearMap.GeneralLinearGroup Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring LinearMap Module.End.instMonoid MulEquiv.instEquivLike toLin' Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike Fintype.linearCombination Module.Basis Module.Basis.instFunLike Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr	—	RingHomInvPair.ids Module.Basis.equivFun_symm_apply
toLin_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike Units.val Module.End.instMonoid MulEquiv Matrix.GeneralLinearGroup LinearMap.GeneralLinearGroup Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring EquivLike.toFunLike MulEquiv.instEquivLike toLin NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.mulVecLin	—	—
val_det_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike det Matrix.det	—	—
val_inv_det_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv DFunLike.coe MonoidHom Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike det Matrix.det	—	—
val_inv_scalar_apply 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Units Units.instInv DFunLike.coe MonoidHom Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike scalar Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
val_map_apply 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike map Matrix.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—
val_mk' 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring mk'	—	—
val_mk'' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det	Units.val Matrix Matrix.semiring mk''	—	—
val_mkOfDetNeZero 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield mkOfDetNeZero	—	—
val_scalar_apply 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom Units Matrix.GeneralLinearGroup MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike scalar Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—

Matrix.IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kronecker 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring	instFintypeProd Matrix.kroneckerMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Units.isUnit

Matrix.SpecialLinearGroup

Definitions

Name	Category	Theorems
hasCoeToGeneralLinearGroup 📖	CompOp	—
instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos 📖	CompOp	—
mapGL 📖	CompOp	50 math math: map_mapGL, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, CongruenceSubgroup.exists_Gamma_le_conj', CongruenceSubgroup.strictPeriods_Gamma0, ModularForm.levelOne_neg_weight_rank_zero, Subgroup.IsArithmetic.is_commensurable, CongruenceSubgroup.exists_Gamma_le_conj, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff', Subgroup.strictWidthInfty_eq_one_of_T_mem, mapGL_injective, ModularFormClass.one_mem_strictPeriods_SL2Z, mapGL_inj, ModularForm.levelOne_weight_zero_rank_one, CongruenceSubgroup.strictWidthInfty_Gamma0, isClosedEmbedding_mapGLInt, Subgroup.IsArithmetic.isFiniteRelIndexSL, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, CongruenceSubgroup.isArithmetic_conj_SL2Z, EisensteinSeries.q_expansion_riemannZeta, isInducing_mapGL, Subgroup.isArithmetic_iff_finiteIndex, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, isCusp_SL2Z_iff, surjective_cosetToCuspOrbit, CongruenceSubgroup.strictWidthInfty_Gamma1, EisensteinSeries.eisensteinSeries_SIF_apply, CongruenceSubgroup.strictPeriods_Gamma1, CongruenceSubgroup.strictWidthInfty_Gamma, EisensteinSeries.q_expansion_bernoulli, CongruenceSubgroup.strictPeriods_Gamma, cosetToCuspOrbit_apply_mk, OnePoint.exists_mem_SL2, Subgroup.strictPeriods_SL2Z, SlashInvariantForm.vAdd_width_periodic, EisensteinSeries.eisensteinSeriesSIF_apply, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, mapGL_coe_matrix, Subgroup.IsArithmetic.finiteIndex_comap, det_mapGL, discreteSpecialLinearGroupIntRange, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, Subgroup.strictWidthInfty_SL2Z, isEmbedding_mapGL, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF
toGL 📖	CompOp	25 math math: continuous_toGL, coeToGL_det, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, ModularGroup.sl_moeb, isClosedEmbedding_toGL, ModularGroup.denom_apply, ModularGroup.denom_S, CuspForm.coe_translate, toGL_injective, range_toGL, isEmbedding_toGL, ModularForm.SL_slash_def, SlashInvariantForm.slash_action_eqn_SL'', ModularGroup.im_smul_eq_div_normSq, coe_GL_coe_matrix, CongruenceSubgroup.mem_conjGL, CongruenceSubgroup.mem_conjGL', ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, ModularForm.is_invariant_one', ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, isInducing_toGL, toGL_inj
toGLPos 📖	CompOp	4 math math: toGLPos_injective, coe_GLPos_neg, coe_to_GLPos_to_GL_det, coe_GLPos_coe_GL_coe_matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeToGL_det 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Matrix.SpecialLinearGroup Monoid.toMulOneClass monoid toGL Units.instOne	—	Units.ext Subtype.prop
coe_GLPos_coe_GL_coe_matrix 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.GeneralLinearGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos DFunLike.coe MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike toGLPos Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
coe_GLPos_neg 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike toGLPos instNeg Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos	—	Units.ext
coe_GL_coe_matrix 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike toGL Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
coe_to_GLPos_to_GL_det 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Matrix.SpecialLinearGroup Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup toGLPos Units.instOne	—	Units.ext Subtype.prop
det_mapGL 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Matrix.SpecialLinearGroup Monoid.toMulOneClass monoid mapGL Units.instOne	—	coeToGL_det
mapGL_coe_matrix 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike mapGL Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing map algebraMap	—	—
mapGL_inj 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike mapGL	—	—
mapGL_injective 📖	mathematical	—	Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike mapGL	—	—
map_mapGL 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.map algebraMap Matrix.SpecialLinearGroup Monoid.toMulOneClass monoid mapGL	—	Units.ext Matrix.ext Matrix.GeneralLinearGroup.map_apply IsScalarTower.algebraMap_apply
toGLPos_injective 📖	mathematical	—	Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike toGLPos	—	Function.Injective.of_comp Subtype.coe_injective
toGL_inj 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike toGL	—	toGL_injective
toGL_injective 📖	mathematical	—	Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike toGL	—	—

MatrixGroups

Definitions

Name	Category	Theorems
«termGL(_,_)⁺» 📖⁺» "API Documentation")	CompOp	—

---

← Back to Index