SpecialLinearGroup

📁 Source: Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Statistics

Metric	Count
Definitions SpecialLinearGroup, center_equiv_rootsOfUnity, center_equiv_rootsOfUnity', hasCoeToMatrix, hasInv, hasMul, hasOne, instCoeFun, instCoeInt, instFintypeOfDecidableEq, instGroup, instHasDistribNeg, instInhabited, instNeg, instPowNat, map, monoid, toLin', transpose, «term_ᵀ», «termSL(_,_)»»), S, T	23
Theorems exists_SL2_col, exists_SL2_row, mulVecSL, vecMulSL, SL2_inv_expl, SL2_inv_expl_det, center_eq_bot_of_subsingleton, center_equiv_rootsOfUnity'_apply, center_equiv_rootsOfUnity'_symm_apply_coe_coe, coe_int_neg, coe_inv, coe_matrix_coe, coe_mk, coe_mul, coe_neg, coe_one, coe_pow, coe_transpose, det_coe, det_ne_zero, eq_scalar_center_equiv_rootsOfUnity, ext, ext_iff, fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, fin_two_induction, instFinite, isCoprime_col, isCoprime_row, map_apply_coe, map_intCast_inj, map_intCast_injective, mem_center_iff, row_ne_zero, scalar_eq_coe_self_center, scalar_eq_self_of_mem_center, subsingleton_of_subsingleton, toLin'_apply, toLin'_injective, toLin'_symm_apply, toLin'_symm_to_linearMap, toLin'_to_linearMap, S_mul_S_eq, T_S_rel, T_inv_mul_apply_one, T_mul_apply_one, T_pow_mul_apply_one, coe_S, coe_T, coe_T_inv, coe_T_zpow	50
Total	73

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_SL2_col 📖	mathematical	IsCoprime CommRing.toCommSemiring	Matrix Matrix.det Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det_fin_two_of Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt
exists_SL2_row 📖	mathematical	IsCoprime CommRing.toCommSemiring	Matrix Matrix.det Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det_fin_two_of Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt
mulVecSL 📖	mathematical	IsCoprime CommRing.toCommSemiring	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fin.fintype Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	vecMulSL
vecMulSL 📖	mathematical	IsCoprime CommRing.toCommSemiring	Matrix.vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fin.fintype Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	exists_SL2_row Fintype.complete Matrix.SpecialLinearGroup.isCoprime_row

Matrix

Definitions

Name	Category	Theorems
SpecialLinearGroup 📖	CompOp	195 math math: CongruenceSubgroup.Gamma_zero_bot, ModularForm.mul_slash_SL2, ModularGroup.SLOnGLPos_smul_apply, SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, SpecialLinearGroup.map_mapGL, SpecialLinearGroup.continuous_toGL, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, CongruenceSubgroup.Gamma_mem', SpecialLinearGroup.coeToGL_det, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, SpecialLinearGroup.toGLPos_injective, CongruenceSubgroup.instFiniteIndexGamma, SpecialLinearGroup.topologicalGroup, CongruenceSubgroup.exists_Gamma_le_conj', ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, CongruenceSubgroup.mem_Gamma_one, UpperHalfPlane.specialLinearGroup_apply, ModularGroup.one_lt_normSq_T_zpow_smul, ModularGroup.bottom_row_surj, CongruenceSubgroup.strictPeriods_Gamma0, SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, CongruenceSubgroup.Gamma_normal, SpecialLinearGroup.map_intCast_injective, jacobiTheta_T_sq_smul, ModularForm.levelOne_neg_weight_rank_zero, Subgroup.IsArithmetic.is_commensurable, ModularGroup.sl_moeb, SpecialLinearGroup.center_eq_bot_of_subsingleton, SpecialLinearGroup.coe_int_neg, EisensteinSeries.E2_slash_action, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, ModularGroup.coe_T_zpow_smul_eq, CongruenceSubgroup.exists_Gamma_le_conj, EisensteinSeries.G2_slash_action, ModularGroup.g_eq_of_c_eq_one, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, SpecialLinearGroup.isClosedEmbedding_toGL, SpecialLinearGroup.coe_one, ModularGroup.tendsto_abs_re_smul, CongruenceSubgroup.Gamma1_mem', SpecialLinearGroup.instFinite, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, SpecialLinearGroup.toLin'_symm_to_linearMap, ModularGroup.exists_max_im, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, CongruenceSubgroup.instFiniteIndexGamma1, isCusp_SL2Z_iff', ModularGroup.denom_apply, FixedDetMatrices.reduce_of_pos, ModularGroup.im_T_smul, SpecialLinearGroup.map_apply_coe, FixedDetMatrices.T_S_rel_smul, CongruenceSubgroup.Gamma_one_top, SpecialLinearGroup.instDiscreteTopology, EisensteinSeries.G2_S_transform, SpecialLinearGroup.mapGL_injective, ModularGroup.SL_to_GL_tower, ModularFormClass.one_mem_strictPeriods_SL2Z, ModularGroup.T_mul_apply_one, SpecialLinearGroup.mapGL_inj, jacobiTheta_S_smul, ModularForm.levelOne_weight_zero_rank_one, ModularGroup.re_T_smul, CongruenceSubgroup.strictWidthInfty_Gamma0, CongruenceSubgroup.Gamma_cong_eq_self, ModularGroup.coe_T_inv, ModularGroup.T_inv_mul_apply_one, SpecialLinearGroup.isClosedEmbedding_mapGLInt, Subgroup.IsArithmetic.isFiniteRelIndexSL, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero, UpperHalfPlane.modular_S_smul, ModularGroup.re_T_inv_smul, EisensteinSeries.D2_inv, CongruenceSubgroup.isArithmetic_conj_SL2Z, EisensteinSeries.q_expansion_riemannZeta, ModularGroup.denom_S, SpecialLinearGroup.subsingleton_of_subsingleton, SpecialLinearGroup.isInducing_mapGL, ModularGroup.normSq_S_smul_lt_one, ModularGroup.T_pow_mul_apply_one, ModularGroup.exists_row_one_eq_and_min_re, SpecialLinearGroup.scalar_eq_coe_self_center, ModularGroup.re_T_zpow_smul, CuspForm.coe_translate, SpecialLinearGroup.SL2Z_generators, ModularGroup.im_lt_im_S_smul, Subgroup.isArithmetic_iff_finiteIndex, SpecialLinearGroup.toGL_injective, ModularGroup.im_T_zpow_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, EisensteinSeries.vecMul_SL2_mem_gammaSet, isCusp_SL2Z_iff, ModularForm.slash_action_eq'_iff, surjective_cosetToCuspOrbit, CongruenceSubgroup.strictWidthInfty_Gamma1, SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, SpecialLinearGroup.SL2_inv_expl, EisensteinSeries.eisensteinSeries_SIF_apply, UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, SpecialLinearGroup.coe_inv, CongruenceSubgroup.finiteIndex_conjGL, SpecialLinearGroup.range_toGL, ModularGroup.exists_one_half_le_im_smul, CongruenceSubgroup.instFiniteIndexGamma0, SpecialLinearGroup.isEmbedding_toGL, SpecialLinearGroup.coe_GLPos_neg, SpecialLinearGroup.coe_pow, UpperHalfPlane.petersson_slash_SL, CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma, ModularForm.SL_slash_def, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero, CongruenceSubgroup.strictPeriods_Gamma1, CongruenceSubgroup.strictWidthInfty_Gamma, UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, EisensteinSeries.q_expansion_bernoulli, UpperHalfPlane.coe_specialLinearGroup_apply, EisensteinSeries.D2_one, CongruenceSubgroup.Gamma1_in_Gamma0, CongruenceSubgroup.Gamma1_mem, ModularGroup.im_smul_eq_div_normSq, SpecialLinearGroup.coe_GL_coe_matrix, SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, CongruenceSubgroup.mem_conjGL, SpecialLinearGroup.map_intCast_inj, SpecialLinearGroup.coe_to_GLPos_to_GL_det, SpecialLinearGroup.toLin'_to_linearMap, EisensteinSeries.tendsto_double_sum_S_act, CongruenceSubgroup.strictPeriods_Gamma, ModularGroup.tendsto_lcRow0, cosetToCuspOrbit_apply_mk, OnePoint.exists_mem_SL2, SL_reduction_mod_hom_val, SlashInvariantForm.slash_S_apply, ModularGroup.coe_one, CongruenceSubgroup.Gamma1_to_Gamma0_mem, Subgroup.strictPeriods_SL2Z, CongruenceSubgroup.mem_conjGL', FixedDetMatrices.smul_def, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, ModularGroup.T_S_rel, SpecialLinearGroup.toLin_equiv.toLinearMap_eq, FixedDetMatrices.reduce_of_not_pos, SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SlashInvariantForm.vAdd_width_periodic, ModularGroup.exists_smul_mem_fd, ModularFormClass.bdd_at_infty_slash, CuspFormClass.zero_at_infty_slash, CongruenceSubgroup.conj_cong_is_cong, ModularForm.is_invariant_one', EisensteinSeries.eisensteinSeriesSIF_apply, ModularGroup.im_T_inv_smul, SpecialLinearGroup.coe_neg, UpperHalfPlane.modular_T_zpow_smul, SpecialLinearGroup.toLin'_injective, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex, SpecialLinearGroup.coe_matrix_coe, FixedDetMatrices.smul_coe, SpecialLinearGroup.mapGL_coe_matrix, ModularForm.is_invariant_const, Subgroup.IsArithmetic.finiteIndex_comap, SpecialLinearGroup.det_mapGL, ModularForm.SL_slash_apply, SpecialLinearGroup.discreteSpecialLinearGroupIntRange, EisensteinSeries.eisSummand_SL2_apply, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, SpecialLinearGroup.toLin'_symm_apply, ModularGroup.coe_T_zpow, EisensteinSeries.eisensteinSeries_slash_apply, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, CongruenceSubgroup.Gamma_mem, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, SpecialLinearGroup.coe_mul, ModularGroup.coeHom_apply, Subgroup.strictWidthInfty_SL2Z, SpecialLinearGroup.isInducing_toGL, ModularGroup.SL_neg_smul, FixedDetMatrices.reps_one_id, ModularForm.is_invariant_one, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, EisensteinSeries.D2_mul, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, UpperHalfPlane.modular_T_smul, SpecialLinearGroup.toGL_inj, ModularGroup.smul_eq_lcRow0_add, SpecialLinearGroup.toLin'_apply, ModularForm.SL_smul_slash, SpecialLinearGroup.mem_center_iff, SpecialLinearGroup.isEmbedding_mapGL, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, CongruenceSubgroup.Gamma0_mem, EisensteinSeries.G2_T_transform, FixedDetMatrices.S_smul_four

Matrix.SpecialLinearGroup

Definitions

Name	Category	Theorems
center_equiv_rootsOfUnity 📖	CompOp	2 math math: SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, eq_scalar_center_equiv_rootsOfUnity
center_equiv_rootsOfUnity' 📖	CompOp	2 math math: center_equiv_rootsOfUnity'_apply, center_equiv_rootsOfUnity'_symm_apply_coe_coe
hasCoeToMatrix 📖	CompOp	—
hasInv 📖	CompOp	13 math math: CongruenceSubgroup.conjGL_coe, toLin'_symm_to_linearMap, FixedDetMatrices.T_S_rel_smul, ModularGroup.coe_T_inv, ModularGroup.T_inv_mul_apply_one, ModularGroup.re_T_inv_smul, EisensteinSeries.D2_inv, SL2_inv_expl, coe_inv, cosetToCuspOrbit_apply_mk, ModularGroup.T_S_rel, ModularGroup.im_T_inv_smul, toLin'_symm_apply
hasMul 📖	CompOp	8 math math: ModularGroup.g_eq_of_c_eq_one, ModularGroup.T_mul_apply_one, ModularGroup.T_inv_mul_apply_one, ModularGroup.T_pow_mul_apply_one, toLin_equiv.symm_toLinearMap_eq, toLin_equiv.toLinearMap_eq, coe_mul, EisensteinSeries.D2_mul
hasOne 📖	CompOp	5 math math: CongruenceSubgroup.Gamma_mem', coe_one, EisensteinSeries.D2_one, ModularGroup.coe_one, FixedDetMatrices.reps_one_id
instCoeFun 📖	CompOp	—
instCoeInt 📖	CompOp	—
instFintypeOfDecidableEq 📖	CompOp	—
instGroup 📖	CompOp	83 math math: CongruenceSubgroup.Gamma_zero_bot, center_equiv_rootsOfUnity'_apply, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, CongruenceSubgroup.Gamma_mem', Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, CongruenceSubgroup.instFiniteIndexGamma, topologicalGroup, CongruenceSubgroup.exists_Gamma_le_conj', CongruenceSubgroup.conjGL_coe, CongruenceSubgroup.mem_Gamma_one, ModularGroup.one_lt_normSq_T_zpow_smul, CongruenceSubgroup.strictPeriods_Gamma0, center_equiv_rootsOfUnity'_symm_apply_coe_coe, CongruenceSubgroup.Gamma_normal, ModularForm.levelOne_neg_weight_rank_zero, Subgroup.IsArithmetic.is_commensurable, center_eq_bot_of_subsingleton, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, ModularGroup.coe_T_zpow_smul_eq, CongruenceSubgroup.exists_Gamma_le_conj, ModularGroup.g_eq_of_c_eq_one, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, CongruenceSubgroup.Gamma1_mem', Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, CongruenceSubgroup.instFiniteIndexGamma1, isCusp_SL2Z_iff', FixedDetMatrices.reduce_of_pos, CongruenceSubgroup.Gamma_one_top, ModularFormClass.one_mem_strictPeriods_SL2Z, ModularForm.levelOne_weight_zero_rank_one, CongruenceSubgroup.strictWidthInfty_Gamma0, CongruenceSubgroup.Gamma_cong_eq_self, Subgroup.IsArithmetic.isFiniteRelIndexSL, CongruenceSubgroup.isArithmetic_conj_SL2Z, EisensteinSeries.q_expansion_riemannZeta, ModularGroup.T_pow_mul_apply_one, scalar_eq_coe_self_center, ModularGroup.re_T_zpow_smul, SpecialLinearGroup.SL2Z_generators, Subgroup.isArithmetic_iff_finiteIndex, ModularGroup.im_T_zpow_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, isCusp_SL2Z_iff, surjective_cosetToCuspOrbit, CongruenceSubgroup.strictWidthInfty_Gamma1, EisensteinSeries.eisensteinSeries_SIF_apply, CongruenceSubgroup.finiteIndex_conjGL, CongruenceSubgroup.instFiniteIndexGamma0, CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma, CongruenceSubgroup.strictPeriods_Gamma1, CongruenceSubgroup.strictWidthInfty_Gamma, UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, EisensteinSeries.q_expansion_bernoulli, CongruenceSubgroup.Gamma1_in_Gamma0, CongruenceSubgroup.Gamma1_mem, eq_scalar_center_equiv_rootsOfUnity, CongruenceSubgroup.mem_conjGL, CongruenceSubgroup.strictPeriods_Gamma, cosetToCuspOrbit_apply_mk, CongruenceSubgroup.Gamma1_to_Gamma0_mem, Subgroup.strictPeriods_SL2Z, CongruenceSubgroup.mem_conjGL', FixedDetMatrices.reduce_of_not_pos, SlashInvariantForm.vAdd_width_periodic, CongruenceSubgroup.conj_cong_is_cong, EisensteinSeries.eisensteinSeriesSIF_apply, UpperHalfPlane.modular_T_zpow_smul, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex, Subgroup.IsArithmetic.finiteIndex_comap, discreteSpecialLinearGroupIntRange, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, ModularGroup.coe_T_zpow, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, CongruenceSubgroup.Gamma_mem, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, Subgroup.strictWidthInfty_SL2Z, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, mem_center_iff, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, CongruenceSubgroup.Gamma0_mem
instHasDistribNeg 📖	CompOp	—
instInhabited 📖	CompOp	—
instNeg 📖	CompOp	4 math math: coe_int_neg, coe_GLPos_neg, coe_neg, ModularGroup.SL_neg_smul
instPowNat 📖	CompOp	1 math math: coe_pow
map 📖	CompOp	27 math math: CongruenceSubgroup.Gamma_mem', ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, map_intCast_injective, ModularGroup.sl_moeb, coe_int_neg, ModularGroup.denom_apply, map_apply_coe, ModularGroup.denom_S, CuspForm.coe_translate, EisensteinSeries.vecMul_SL2_mem_gammaSet, ModularForm.SL_slash_def, SlashInvariantForm.slash_action_eqn_SL'', ModularGroup.im_smul_eq_div_normSq, CongruenceSubgroup.mem_conjGL, map_intCast_inj, ModularGroup.tendsto_lcRow0, SL_reduction_mod_hom_val, CongruenceSubgroup.mem_conjGL', ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, ModularForm.is_invariant_one', coe_matrix_coe, mapGL_coe_matrix, ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, EisensteinSeries.eisensteinSeries_slash_apply, ModularGroup.smul_eq_lcRow0_add
monoid 📖	CompOp	111 math math: ModularForm.mul_slash_SL2, map_mapGL, continuous_toGL, CongruenceSubgroup.Gamma_mem', coeToGL_det, OnePoint.isBoundedAt_iff_exists_SL2Z, toGLPos_injective, ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, UpperHalfPlane.specialLinearGroup_apply, ModularGroup.one_lt_normSq_T_zpow_smul, map_intCast_injective, jacobiTheta_T_sq_smul, OnePoint.isBoundedAt_iff_forall_SL2Z, ModularGroup.sl_moeb, coe_int_neg, OnePoint.isZeroAt_iff_exists_SL2Z, EisensteinSeries.E2_slash_action, ModularGroup.coe_T_zpow_smul_eq, CongruenceSubgroup.exists_Gamma_le_conj, EisensteinSeries.G2_slash_action, isClosedEmbedding_toGL, ModularGroup.tendsto_abs_re_smul, toLin'_symm_to_linearMap, ModularGroup.exists_max_im, isCusp_SL2Z_iff', ModularGroup.denom_apply, ModularGroup.im_T_smul, map_apply_coe, EisensteinSeries.G2_S_transform, mapGL_injective, ModularGroup.SL_to_GL_tower, mapGL_inj, jacobiTheta_S_smul, ModularGroup.re_T_smul, isClosedEmbedding_mapGLInt, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero, UpperHalfPlane.modular_S_smul, ModularGroup.re_T_inv_smul, EisensteinSeries.D2_inv, ModularGroup.denom_S, OnePoint.isZeroAt_iff_forall_SL2Z, isInducing_mapGL, ModularGroup.normSq_S_smul_lt_one, ModularGroup.exists_row_one_eq_and_min_re, ModularGroup.re_T_zpow_smul, CuspForm.coe_translate, ModularGroup.im_lt_im_S_smul, toGL_injective, ModularGroup.im_T_zpow_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, EisensteinSeries.vecMul_SL2_mem_gammaSet, ModularForm.slash_action_eq'_iff, UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, range_toGL, ModularGroup.exists_one_half_le_im_smul, isEmbedding_toGL, coe_GLPos_neg, UpperHalfPlane.petersson_slash_SL, ModularForm.SL_slash_def, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero, SlashInvariantForm.slash_action_eqn_SL'', UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, UpperHalfPlane.coe_specialLinearGroup_apply, ModularGroup.im_smul_eq_div_normSq, coe_GL_coe_matrix, CongruenceSubgroup.mem_conjGL, map_intCast_inj, coe_to_GLPos_to_GL_det, toLin'_to_linearMap, EisensteinSeries.tendsto_double_sum_S_act, ModularGroup.tendsto_lcRow0, cosetToCuspOrbit_apply_mk, OnePoint.exists_mem_SL2, SL_reduction_mod_hom_val, SlashInvariantForm.slash_S_apply, CongruenceSubgroup.mem_conjGL', ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, ModularGroup.T_S_rel, coe_GLPos_coe_GL_coe_matrix, ModularGroup.exists_smul_mem_fd, ModularFormClass.bdd_at_infty_slash, CuspFormClass.zero_at_infty_slash, ModularForm.is_invariant_one', ModularGroup.im_T_inv_smul, UpperHalfPlane.modular_T_zpow_smul, toLin'_injective, coe_matrix_coe, mapGL_coe_matrix, ModularForm.is_invariant_const, det_mapGL, ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, toLin'_symm_apply, EisensteinSeries.eisensteinSeries_slash_apply, ModularGroup.coeHom_apply, isInducing_toGL, ModularGroup.SL_neg_smul, ModularForm.is_invariant_one, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, EisensteinSeries.D2_mul, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, UpperHalfPlane.modular_T_smul, toGL_inj, ModularGroup.smul_eq_lcRow0_add, toLin'_apply, ModularForm.SL_smul_slash, isEmbedding_mapGL, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, EisensteinSeries.G2_T_transform
toLin' 📖	CompOp	5 math math: toLin'_symm_to_linearMap, toLin'_to_linearMap, toLin'_injective, toLin'_symm_apply, toLin'_apply
transpose 📖	CompOp	1 math math: coe_transpose
«term_ᵀ» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SL2_inv_expl 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype hasInv Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecCons NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Matrix.vecEmpty SL2_inv_expl_det	—	ext SL2_inv_expl_det Matrix.adjugate_fin_two coe_inv Matrix.cons_val' Matrix.cons_val_fin_one
SL2_inv_expl_det 📖	mathematical	—	Matrix.det Fin.fintype Matrix.vecCons Matrix AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Matrix.vecEmpty	—	Matrix.det_fin_two Matrix.cons_val' Matrix.cons_val_fin_one mul_comm mul_neg neg_mul neg_neg
center_eq_bot_of_subsingleton 📖	mathematical	—	Subgroup.center Matrix.SpecialLinearGroup instGroup Bot.bot Subgroup Subgroup.instBot	—	eq_bot_iff Subgroup.mem_bot subsingleton_of_subsingleton
center_equiv_rootsOfUnity'_apply 📖	mathematical	—	DFunLike.coe MulEquiv Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center Units CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup rootsOfUnity Fintype.card Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike center_equiv_rootsOfUnity' rootsOfUnity.mkOfPowEq Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
center_equiv_rootsOfUnity'_symm_apply_coe_coe 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center DFunLike.coe MulEquiv Units CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup rootsOfUnity Fintype.card Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm center_equiv_rootsOfUnity' Matrix.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
coe_int_neg 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Int.instCommRing MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing instNeg	—	RingHom.map_neg
coe_inv 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup hasInv Matrix.adjugate	—	—
coe_matrix_coe 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Int.instCommRing MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Matrix.map RingHom Semiring.toNonAssocSemiring Int.instSemiring NonAssocRing.toNonAssocSemiring RingHom.instFunLike	—	map_apply_coe
coe_mk 📖	mathematical	Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Matrix	—	—
coe_mul 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup hasMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	—
coe_neg 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup instNeg Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—
coe_one 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup hasOne Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
coe_pow 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup instPowNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
coe_transpose 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing transpose Matrix.transpose	—	—
det_coe 📖	mathematical	—	Matrix.det Matrix AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
det_ne_zero 📖	—	—	—	—	det_coe NeZero.one
eq_scalar_center_equiv_rootsOfUnity 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Units.instGroup rootsOfUnity Fintype.card MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike center_equiv_rootsOfUnity	—	isEmpty_or_nonempty Matrix.subsingleton_of_empty_right center_equiv_rootsOfUnity'_apply rootsOfUnity.val_mkOfPowEq_coe scalar_eq_coe_self_center
ext 📖	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	ext_iff
ext_iff 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.ext_iff
fin_two_exists_eq_mk_of_apply_zero_one_eq_zero 📖	mathematical	Matrix Matrix.det Fin.fintype Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	fin_two_induction Matrix.cons_val' Matrix.cons_val_fin_one sub_zero MulZeroClass.mul_zero left_ne_zero_of_mul_eq_one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing eq_inv_of_mul_eq_one_right
fin_two_induction 📖	—	Matrix Matrix.det Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty	—	—	Matrix.det_fin_two Matrix.ext Fintype.complete
instFinite 📖	mathematical	—	Finite Matrix.SpecialLinearGroup	—	Subtype.finite Matrix.instFinite Finite.of_fintype
isCoprime_col 📖	mathematical	—	IsCoprime CommRing.toCommSemiring Matrix Matrix.det Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det_fin_two det_coe Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
isCoprime_row 📖	mathematical	—	IsCoprime CommRing.toCommSemiring Matrix Matrix.det Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det_fin_two det_coe Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
map_apply_coe 📖	mathematical	—	Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike map RingHom Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.mapMatrix	—	—
map_intCast_inj 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Int.instCommRing MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	map_intCast_injective
map_intCast_injective 📖	mathematical	—	Matrix.SpecialLinearGroup Int.instCommRing DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	—
mem_center_iff 📖	mathematical	—	Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Fintype.card AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Matrix.det	—	isEmpty_or_nonempty Fintype.card_eq_zero pow_zero center_eq_bot_of_subsingleton IsEmpty.instSubsingleton subsingleton_of_subsingleton SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass scalar_eq_self_of_mem_center Matrix.det_diagonal Finset.prod_const Subgroup.mem_center_iff Commute.symm Matrix.scalar_commute Commute.all Subtype.val_injective
row_ne_zero 📖	—	—	—	—	det_ne_zero Matrix.det_eq_zero_of_row_eq_zero
scalar_eq_coe_self_center 📖	mathematical	—	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center	—	scalar_eq_self_of_mem_center
scalar_eq_self_of_mem_center 📖	mathematical	Matrix.SpecialLinearGroup Subgroup instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.center	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.mem_range_scalar_of_commute_transvectionStruct Matrix.TransvectionStruct.det Subgroup.mem_center_iff Matrix.diagonal_apply_eq
subsingleton_of_subsingleton 📖	mathematical	—	Matrix.SpecialLinearGroup	—	ext isEmpty_or_nonempty IsEmpty.false Matrix.det_eq_elem_of_subsingleton
toLin'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toLin' LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike Matrix Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.toLin' Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids
toLin'_injective 📖	mathematical	—	Matrix.SpecialLinearGroup LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toLin'	—	RingHomInvPair.ids Subtype.coe_injective LinearEquiv.injective Function.smulCommClass Algebra.to_smulCommClass LinearEquiv.toLinearMap_injective
toLin'_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toLin' LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike Matrix Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.toLin' Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing hasInv	—	RingHomInvPair.ids
toLin'_symm_to_linearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearEquiv.symm DFunLike.coe MonoidHom Matrix.SpecialLinearGroup LinearEquiv MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toLin' Matrix LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin' Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing hasInv	—	RingHomInvPair.ids
toLin'_to_linearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule DFunLike.coe MonoidHom Matrix.SpecialLinearGroup LinearEquiv MulOneClass.toMulOne Monoid.toMulOneClass monoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toLin' Matrix LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin' Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids

MatrixGroups

Definitions

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

ModularGroup

Definitions

Name	Category	Theorems
S 📖	CompOp	19 math math: g_eq_of_c_eq_one, FixedDetMatrices.T_S_rel_smul, EisensteinSeries.D2_S, EisensteinSeries.G2_S_transform, jacobiTheta_S_smul, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero, UpperHalfPlane.modular_S_smul, denom_S, normSq_S_smul_lt_one, SpecialLinearGroup.SL2Z_generators, im_lt_im_S_smul, EisensteinSeries.tendsto_double_sum_S_act, SlashInvariantForm.slash_S_apply, T_S_rel, FixedDetMatrices.reduce_of_not_pos, coe_S, S_mul_S_eq, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, FixedDetMatrices.S_smul_four
T 📖	CompOp	29 math math: one_lt_normSq_T_zpow_smul, jacobiTheta_T_sq_smul, coe_T_zpow_smul_eq, g_eq_of_c_eq_one, FixedDetMatrices.reduce_of_pos, im_T_smul, FixedDetMatrices.T_S_rel_smul, T_mul_apply_one, re_T_smul, coe_T_inv, T_inv_mul_apply_one, re_T_inv_smul, T_pow_mul_apply_one, re_T_zpow_smul, SpecialLinearGroup.SL2Z_generators, im_T_zpow_smul, CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma, UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, T_S_rel, FixedDetMatrices.reduce_of_not_pos, coe_T, im_T_inv_smul, UpperHalfPlane.modular_T_zpow_smul, coe_T_zpow, EisensteinSeries.D2_T, exists_eq_T_zpow_of_c_eq_zero, UpperHalfPlane.modular_T_smul, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.G2_T_transform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
S_mul_S_eq 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Int.instAddCommMonoid Matrix.det Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing S Matrix.neg Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instRing	—	Matrix.cons_mul Matrix.vecMul_cons zero_smul Matrix.tail_cons neg_smul one_smul Matrix.neg_cons neg_zero Matrix.neg_empty add_zero zero_add Matrix.empty_mul Equiv.symm_apply_apply Matrix.eta_fin_two
T_S_rel 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction Monoid.toMulAction S T Matrix.SpecialLinearGroup.hasInv	—	Matrix.SpecialLinearGroup.ext Fintype.complete
T_inv_mul_apply_one 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.hasMul Matrix.SpecialLinearGroup.hasInv T	—	zpow_neg zpow_one T_pow_mul_apply_one
T_mul_apply_one 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.hasMul T	—	zpow_one T_pow_mul_apply_one
T_pow_mul_apply_one 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.hasMul DivInvMonoid.toZPow Group.toDivInvMonoid Matrix.SpecialLinearGroup.instGroup T	—	coe_T_zpow Matrix.cons_mul Matrix.empty_mul Equiv.symm_apply_apply Matrix.cons_val' Finset.sum_congr Fin.sum_univ_succ one_mul Finset.univ_unique Matrix.cons_val_succ Matrix.cons_val_fin_one Finset.sum_singleton MulZeroClass.zero_mul zero_add
coe_S 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing S DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty	—	—
coe_T 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing T DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty	—	—
coe_T_inv 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.hasInv T DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty	—	Matrix.adjugate_fin_two Matrix.cons_val' Matrix.cons_val_fin_one neg_zero
coe_T_zpow 📖	mathematical	—	Matrix Matrix.det Fin.fintype Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.SpecialLinearGroup DivInvMonoid.toZPow Group.toDivInvMonoid Matrix.SpecialLinearGroup.instGroup T DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Matrix.vecEmpty	—	Int.induction_on zpow_zero Matrix.SpecialLinearGroup.coe_one Matrix.one_fin_two zpow_add zpow_one Matrix.mul_fin_two mul_one add_comm zpow_sub coe_T_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt

---

← Back to Index