MoebiusAction

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

Statistics

Metric	Count
Definitions SLOnGLPos, coeHom, instCoeSpecialLinearGroupFinOfNatNatIntSubtypeGeneralLinearGroupRealMemSubgroupGLPos, J, SLAction, denom, glAction, num, smulAux, smulAux', toSL2R, σ	12
Theorems SLOnGLPos_smul_apply, SL_neg_smul, SL_to_GL_tower, coeHom_apply, coe_apply_complex, coe_inj, coe_one, denom_S, denom_apply, det_coe, im_smul_eq_div_normSq, sl_moeb, J_sq, c_mul_im_sq_le_normSq_denom, coe_J_smul, coe_smul, coe_smul_of_det_pos, coe_specialLinearGroup_apply, coe_toSL2R, denom_J, denom_J_mul, denom_cocycle, denom_cocycle', denom_cocycle_σ, denom_ne_zero, denom_ne_zero_of_im, denom_neg, denom_one, det_J, exists_SL2_smul_eq_of_apply_zero_one_eq_zero, exists_SL2_smul_eq_of_apply_zero_one_ne_zero, glPos_smul_def, im_smul, im_smul_eq_div_normSq, isPretransitiveGL2R, isPretransitiveSL2R, linear_ne_zero, linear_ne_zero_of_im, modular_S_smul, modular_T_smul, modular_T_zpow_smul, moebius_im, mul_smul', neg_smul, normSq_denom_ne_zero, normSq_denom_pos, norm_σ, num_neg, re_smul, sigma_J, smulAux'_im, specialLinearGroup_apply, toSL2R_apply, toSL2R_smul_I, val_J, σ_conj, σ_denom, σ_im_ne_zero, σ_mul, σ_mul_comm, σ_neg, σ_num, σ_ofReal, σ_sq	64
Total	76

ModularGroup

Definitions

Name	Category	Theorems
SLOnGLPos 📖	CompOp	2 math math: SLOnGLPos_smul_apply, SL_to_GL_tower
coeHom 📖	CompOp	1 math math: coeHom_apply
instCoeSpecialLinearGroupFinOfNatNatIntSubtypeGeneralLinearGroupRealMemSubgroupGLPos 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SLOnGLPos_smul_apply 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction UpperHalfPlane.glAction Matrix.SpecialLinearGroup Int.instCommRing SLOnGLPos Subgroup.mul coe	—	Real.instIsStrictOrderedRing
SL_neg_smul 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing Matrix.SpecialLinearGroup.instNeg Fintype.card_fin_two	—	Fintype.card_fin_two sl_moeb UpperHalfPlane.neg_smul Units.ext Matrix.ext Matrix.SpecialLinearGroup.coe_int_neg neg_neg
SL_to_GL_tower 📖	mathematical	—	IsScalarTower Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing UpperHalfPlane SLOnGLPos SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction UpperHalfPlane.glAction Matrix.SpecialLinearGroup.monoid UpperHalfPlane.SLAction Ring.toIntAlgebra Real.instRing	—	Real.instIsStrictOrderedRing UpperHalfPlane.mul_smul'
coeHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike coeHom coe	—	Real.instIsStrictOrderedRing
coe_apply_complex 📖	mathematical	—	Complex.ofReal Units.val Matrix Real MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Fin.fintype Units Matrix.GeneralLinearGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing coe Complex Complex.instIntCast Matrix.det Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Real.instIsStrictOrderedRing
coe_inj 📖	mathematical	—	coe	—	Real.instIsStrictOrderedRing Matrix.SpecialLinearGroup.ext RCLike.charZero_rclike
coe_one 📖	mathematical	—	coe Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.hasOne Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing Subgroup.one	—	Real.instIsStrictOrderedRing map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
denom_S 📖	mathematical	—	UpperHalfPlane.denom DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Int.instCommRing Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing S UpperHalfPlane.coe	—	Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one one_mul Int.cast_zero add_zero
denom_apply 📖	mathematical	—	UpperHalfPlane.denom DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Int.instCommRing Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing UpperHalfPlane.coe Complex Complex.instAdd Complex.instMul Complex.instIntCast Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
det_coe 📖	mathematical	—	Matrix.det Fin.fintype Real Real.commRing Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Units Matrix.GeneralLinearGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Matrix.GLPos Real.linearOrder Real.instIsStrictOrderedRing coe Real.instOne	—	Real.instIsStrictOrderedRing Matrix.SpecialLinearGroup.det_coe
im_smul_eq_div_normSq 📖	mathematical	—	UpperHalfPlane.im Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing DivInvMonoid.toDiv Real.instDivInvMonoid DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq UpperHalfPlane.denom MonoidHom Real.commRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing UpperHalfPlane.coe	—	Matrix.SpecialLinearGroup.coeToGL_det abs_one Real.instIsOrderedRing one_mul UpperHalfPlane.im_smul_eq_div_normSq
sl_moeb 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring UpperHalfPlane.glAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	—

UpperHalfPlane

Definitions

Name	Category	Theorems
J 📖	CompOp	9 math math: J_sq, sigma_J, smulFDeriv_J_mul, denom_J, J_smul, coe_J_smul, det_J, val_J, denom_J_mul
SLAction 📖	CompOp	49 math math: specialLinearGroup_apply, ModularGroup.one_lt_normSq_T_zpow_smul, jacobiTheta_T_sq_smul, ModularGroup.sl_moeb, ModularGroup.coe_T_zpow_smul_eq, ModularGroup.tendsto_abs_re_smul, ModularGroup.exists_max_im, ModularGroup.im_T_smul, EisensteinSeries.G2_S_transform, isProperMap_smul_I, ModularGroup.SL_to_GL_tower, jacobiTheta_S_smul, ModularGroup.re_T_smul, exists_SL2_smul_eq_of_apply_zero_one_ne_zero, modular_S_smul, ModularGroup.re_T_inv_smul, ModularGroup.normSq_S_smul_lt_one, ModularGroup.exists_row_one_eq_and_min_re, instProperSMul, ModularGroup.re_T_zpow_smul, ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo, ModularGroup.im_lt_im_S_smul, isPretransitiveSL2R, ModularGroup.im_T_zpow_smul, ModularForm.slash_action_eq'_iff, instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, ModularGroup.exists_one_half_le_im_smul, petersson_slash_SL, ModularForm.SL_slash_def, exists_SL2_smul_eq_of_apply_zero_one_eq_zero, SlashInvariantForm.slash_action_eqn_SL'', ModularGroup_T_zpow_mem_verticalStrip, coe_specialLinearGroup_apply, ModularGroup.im_smul_eq_div_normSq, EisensteinSeries.tendsto_double_sum_S_act, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, ModularGroup.exists_smul_mem_fd, ModularGroup.im_T_inv_smul, modular_T_zpow_smul, ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, instContinuousSMulSL2R, toSL2R_smul_I, ModularGroup.SL_neg_smul, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, modular_T_smul, ModularGroup.smul_eq_lcRow0_add, SlashInvariantForm.T_zpow_width_invariant
denom 📖	CompOp	38 math math: re_smul, deriv_smul, im_smul_eq_div_normSq, moebius_im, glPos_smul_def, denom_cocycle_σ, mdifferentiable_inv_denom, ModularGroup.denom_apply, contMDiff_inv_denom, hasStrictDerivAt_smul, denom_cocycle, coe_smul_of_det_pos, ModularGroup.denom_S, mdifferentiable_denom, im_smul, normSq_denom_pos, coe_smul, denom_J, SlashInvariantForm.slash_action_eqn'', denom_neg, contMDiff_denom_zpow, ModularForm.SL_slash_def, SlashInvariantForm.slash_action_eqn_SL'', ModularGroup.im_smul_eq_div_normSq, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, denom_one, ModularForm.slash_def, denom_J_mul, ModularForm.SL_slash_apply, EisensteinSeries.eisSummand_SL2_apply, denom_cocycle', contMDiff_denom, mdifferentiable_denom_zpow, c_mul_im_sq_le_normSq_denom, smulAux'_im, det_smulFDeriv, σ_denom, ModularForm.slash_apply
glAction 📖	CompOp	32 math math: ModularGroup.SLOnGLPos_smul_apply, instContinuousSMulGL2R, re_smul, analyticAt_smul, instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume, deriv_smul, tendsto_smul_atImInfty, im_smul_eq_div_normSq, ModularGroup.sl_moeb, glPos_smul_def, denom_cocycle_σ, isPretransitiveGL2R, ModularGroup.SL_to_GL_tower, hasStrictDerivAt_smul, coe_smul_of_det_pos, im_smul, coe_smul, J_smul, SlashInvariantForm.slash_action_eqn'', coe_J_smul, meromorphicOrderAt_comp_smul, ModularForm.slash_def, instContinuousGLSMul, SlashInvariantFormClass.norm_petersson_smul, SlashInvariantForm.slash_action_eqn', neg_smul, SlashInvariantFormClass.petersson_smul, contMDiff_smul, hasStrictFDerivAt_smul, mdifferentiable_smul, ModularForm.slash_apply, petersson_slash
num 📖	CompOp	11 math math: mdifferentiable_num, re_smul, num_neg, moebius_im, glPos_smul_def, denom_cocycle, coe_smul_of_det_pos, contMDiff_num, σ_num, im_smul, coe_smul
smulAux 📖	CompOp	2 math math: mul_smul', denom_cocycle'
smulAux' 📖	CompOp	1 math math: smulAux'_im
toSL2R 📖	CompOp	4 math math: coe_toSL2R, continuous_toSL2R, toSL2R_apply, toSL2R_smul_I
σ 📖	CompOp	18 math math: ModularForm.smul_slash, σ_sq, denom_cocycle_σ, σ_mul, norm_σ, sigma_J, σ_num, σ_neg, coe_smul, σ_ofReal, ModularForm.slash_def, σ_conj, denom_cocycle', σ_eventuallyEq, σ_mul_comm, σ_denom, ModularForm.slash_apply, petersson_slash

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
J_sq 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Monoid.toPow Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring J Units.instOne	—	Units.ext Matrix.ext sq Matrix.cons_mul Matrix.vecMul_cons neg_smul one_smul Matrix.neg_cons neg_neg neg_zero Matrix.neg_empty Matrix.tail_cons zero_smul add_zero zero_add Matrix.empty_mul Equiv.symm_apply_apply Matrix.cons_val' Matrix.cons_val_fin_one Matrix.one_fin_two
c_mul_im_sq_le_normSq_denom 📖	mathematical	—	Real Real.instLE Monoid.toPow Real.instMonoid Real.instMul Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Fin.fintype im DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring MonoidWithZeroHom.funLike Complex.normSq denom coe	—	le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.pow_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.sub_neg_of_lt
coe_J_smul 📖	mathematical	—	coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction J Complex Complex.instNeg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Matrix.cons_val' Matrix.cons_val_fin_one Complex.ofReal_neg neg_mul one_mul add_zero MulZeroClass.zero_mul zero_add div_one map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
coe_smul 📖	mathematical	—	coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction DFunLike.coe ContinuousAlgEquiv Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ DivInvMonoid.toDiv Complex.instDivInvMonoid num denom	—	—
coe_smul_of_det_pos 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction Complex DivInvMonoid.toDiv Complex.instDivInvMonoid num denom	—	smulAux'.eq_1 σ.eq_1 ContinuousAlgEquiv.refl_apply num.eq_1 denom.eq_1
coe_specialLinearGroup_apply 📖	mathematical	—	coe Matrix.SpecialLinearGroup Fin.fintype UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instMul Complex.ofReal DFunLike.coe RingHom Real Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring RingHom.instFunLike algebraMap Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	MulAction.compHom_smul_def coe_smul_of_det_pos Matrix.SpecialLinearGroup.det_mapGL Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
coe_toSL2R 📖	mathematical	—	Matrix Real Matrix.det Fin.fintype Real.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing toSL2R DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Real.sqrt im DivInvMonoid.toDiv Real.instDivInvMonoid re Matrix.vecEmpty Real.instZero Real.instOne	—	—
denom_J 📖	mathematical	—	denom J Complex Complex.instOne	—	Matrix.cons_val' Matrix.cons_val_fin_one MulZeroClass.zero_mul zero_add
denom_J_mul 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring J	—	Matrix.cons_mul Matrix.empty_mul Equiv.symm_apply_apply Matrix.cons_val' Matrix.cons_dotProduct neg_mul one_mul MulZeroClass.zero_mul Matrix.dotProduct_of_isEmpty Fin.isEmpty' add_zero zero_add Matrix.cons_val_fin_one
denom_cocycle 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Complex Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid num	—	Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg denom_ne_zero_of_im Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Fin.sum_univ_succ Finset.sum_congr Finset.univ_unique Finset.sum_singleton Complex.ofReal_add Complex.ofReal_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
denom_cocycle' 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring coe Complex Complex.instMul DFunLike.coe ContinuousAlgEquiv Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ smulAux	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass σ_num σ_denom σ_sq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg denom_ne_zero Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Fin.sum_univ_succ Finset.sum_congr Finset.univ_unique Finset.sum_singleton Complex.ofReal_add Complex.ofReal_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
denom_cocycle_σ 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring coe Complex Complex.instMul DFunLike.coe ContinuousAlgEquiv Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction glAction	—	denom_cocycle'
denom_ne_zero 📖	—	—	—	—	denom_ne_zero_of_im im_ne_zero
denom_ne_zero_of_im 📖	—	—	—	—	linear_ne_zero_of_im Units.ne_zero Real.instNontrivial Matrix.det_fin_two MulZeroClass.mul_zero sub_self
denom_neg 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instNeg Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Complex Complex.instNeg	—	Complex.ofReal_neg neg_mul neg_add_rev Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_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_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
denom_one 📖	mathematical	—	denom Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instOne Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring coe Complex Complex.instOne	—	Matrix.one_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 MulZeroClass.zero_mul Matrix.one_apply_eq zero_add
det_J 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det J Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Units.instOne	—	Units.ext Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero
exists_SL2_smul_eq_of_apply_zero_one_eq_zero 📖	mathematical	Matrix Real Matrix.det Fin.fintype Real.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instZero	Real Real.instLT Real.instZero Matrix.SpecialLinearGroup Fin.fintype Real.commRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing posRealAction	—	Real.instIsStrictOrderedRing Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero mul_self_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le ext 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add im_pos coe_specialLinearGroup_apply Matrix.cons_val' Matrix.cons_val_fin_one MulZeroClass.zero_mul map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Complex.ofReal_inv zero_add div_inv_eq_mul add_mul Distrib.rightDistribClass specialLinearGroup_apply Complex.ofReal_mul
exists_SL2_smul_eq_of_apply_zero_one_ne_zero 📖	mathematical	—	Real Real.instLT Real.instZero Matrix.SpecialLinearGroup Fin.fintype Real.commRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Int.instCommRing Ring.toIntAlgebra Real.instRing ModularGroup.S Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing posRealAction	—	denom_ne_zero Matrix.SpecialLinearGroup.fin_two_induction Real.instIsStrictOrderedRing Matrix.cons_val' Matrix.cons_val_fin_one mul_self_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le ext Nat.cast_zero Nat.cast_one coe_specialLinearGroup_apply im_inv_neg_coe_pos inv_neg Complex.ofReal_mul modular_S_smul Complex.ofReal_div
glPos_smul_def 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction Complex DivInvMonoid.toDiv Complex.instDivInvMonoid num coe denom Real.instLT Real.instZero Complex.im im_pos coe_smul_of_det_pos	—	ext im_pos coe_smul_of_det_pos
im_smul 📖	mathematical	—	im Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction abs Real.lattice Real.instAddGroup Complex.im Complex DivInvMonoid.toDiv Complex.instDivInvMonoid num coe denom	—	DFunLike.ite_apply moebius_im abs_div Real.instIsStrictOrderedRing abs_mul Real.instIsOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid im_pos coe_im abs_of_nonneg Complex.normSq_nonneg abs_of_nonpos not_lt
im_smul_eq_div_normSq 📖	mathematical	—	im Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring MonoidWithZeroHom.funLike Complex.normSq denom coe	—	smulAux'_im
isPretransitiveGL2R 📖	mathematical	—	MulAction.IsPretransitive Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction	—	MulAction.IsPretransitive.of_smul_eq isPretransitiveSL2R MulAction.compHom_smul_def
isPretransitiveSL2R 📖	mathematical	—	MulAction.IsPretransitive Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring	—	MulAction.IsPretransitive.of_orbit toSL2R_smul_I
linear_ne_zero 📖	—	—	—	—	linear_ne_zero_of_im im_ne_zero
linear_ne_zero_of_im 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose₄ MulZeroClass.zero_mul add_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Fintype.complete zero_add
modular_S_smul 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Ring.toIntAlgebra Real Real.instRing ModularGroup.S Complex Complex.instInv Complex.instNeg coe im_inv_neg_coe_pos	—	im_inv_neg_coe_pos im_pos coe_specialLinearGroup_apply specialLinearGroup_apply Matrix.cons_val' Matrix.cons_val_fin_one eq_intCast RingHom.instRingHomClass Int.cast_zero MulZeroClass.zero_mul Int.cast_neg Int.cast_one Complex.ofReal_neg zero_add one_mul add_zero neg_div one_div inv_neg
modular_T_smul 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Ring.toIntAlgebra Real Real.instRing ModularGroup.T HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Real.instOne	—	zpow_one Int.cast_one modular_T_zpow_smul
modular_T_zpow_smul 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Ring.toIntAlgebra Real Real.instRing DivInvMonoid.toZPow Group.toDivInvMonoid Matrix.SpecialLinearGroup.instGroup ModularGroup.T HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Real.instIntCast	—	ext_iff coe_vadd add_comm coe_specialLinearGroup_apply ModularGroup.coe_T_zpow Matrix.cons_val' Matrix.cons_val_fin_one eq_intCast RingHom.instRingHomClass Int.cast_one one_mul Int.cast_zero MulZeroClass.zero_mul zero_add div_one
moebius_im 📖	mathematical	—	Complex.im Complex DivInvMonoid.toDiv Complex.instDivInvMonoid num denom Real Real.instDivInvMonoid Real.instMul Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq	—	Complex.div_im MulZeroClass.zero_mul add_zero sub_zero Matrix.det_fin_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr 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.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_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.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_one
mul_smul' 📖	mathematical	—	smulAux Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	ext map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass σ_num σ_mul σ_denom im_ne_zero moebius_im div_ne_zero mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial normSq_denom_ne_zero div_eq_div_iff denom_ne_zero_of_im denom.eq_1 mul_div div_add' num.eq_1 div_mul_eq_mul_div Fin.sum_univ_succ Finset.sum_congr Finset.univ_unique Finset.sum_singleton Complex.ofReal_add Complex.ofReal_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf
neg_smul 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing	—	ext σ_neg num_neg denom_neg neg_div_neg_eq map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass
normSq_denom_ne_zero 📖	—	—	—	—	ne_of_gt normSq_denom_pos
normSq_denom_pos 📖	mathematical	—	Real Real.instLT Real.instZero DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq denom	—	Complex.normSq_pos denom_ne_zero_of_im
norm_σ 📖	mathematical	—	Norm.norm Complex Complex.instNorm DFunLike.coe ContinuousAlgEquiv Real Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ	—	RCLike.norm_conj
num_neg 📖	mathematical	—	num Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instNeg Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Complex Complex.instNeg	—	Complex.ofReal_neg neg_mul neg_add_rev Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_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_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
re_smul 📖	mathematical	—	re Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction Complex.re Complex DivInvMonoid.toDiv Complex.instDivInvMonoid num coe denom	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass DFunLike.ite_apply Complex.div_re Complex.normSq_conj mul_neg neg_mul neg_neg
sigma_J 📖	mathematical	—	σ J Complex.conjCAE	—	Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
smulAux'_im 📖	mathematical	—	Complex.im smulAux' Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul abs Real.lattice Real.instAddGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq denom	—	abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid moebius_im abs_of_nonpos not_lt neg_mul neg_div
specialLinearGroup_apply 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instMul Complex.ofReal DFunLike.coe RingHom Real Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring RingHom.instFunLike algebraMap Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing coe Real.instLT Real.instZero Complex.im im_pos coe_specialLinearGroup_apply	—	ext im_pos coe_specialLinearGroup_apply
toSL2R_apply 📖	mathematical	—	toSL2R Matrix Real Matrix.det Fin.fintype Real.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Real.sqrt im DivInvMonoid.toDiv Real.instDivInvMonoid re Matrix.vecEmpty Real.instZero Real.instOne	—	—
toSL2R_smul_I 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction SLAction Algebra.id CommRing.toCommSemiring toSL2R I	—	im_pos ext div_add' mul_right_comm Complex.ofReal_mul Real.sqrt_mul LT.lt.le Real.sqrt_mul_self re_add_im div_eq_mul_inv coe_specialLinearGroup_apply div_eq_iff Nat.cast_zero denom_ne_zero coe_toSL2R one_div Matrix.cons_val' Matrix.cons_val_fin_one map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Complex.ofReal_div MulZeroClass.zero_mul map_inv₀ Complex.ofReal_inv zero_add add_comm
val_J 📖	mathematical	—	Units.val Matrix Real MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Fin.fintype J DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Real.instNeg Real.instOne Real.instZero Matrix.vecEmpty	—	—
σ_conj 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd
σ_denom 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ denom	—	map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass σ_ofReal
σ_im_ne_zero 📖	—	—	—	—	—
σ_mul 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ Matrix.GeneralLinearGroup Fin.fintype Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Ne.lt_or_gt Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.not_gt RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd mul_neg_of_neg_of_pos mul_neg_of_pos_of_neg IsStrictOrderedRing.toPosMulStrictMono mul_pos
σ_mul_comm 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ	—	RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd
σ_neg 📖	mathematical	—	σ Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instNeg Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing	—	Matrix.det_neg Fintype.card_fin Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow one_mul
σ_num 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ num	—	map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass ContinuousAlgEquivClass.toAlgEquivClass ContinuousAlgEquiv.continuousAlgEquivClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass σ_ofReal
σ_ofReal 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ Complex.ofReal	—	Complex.conj_ofReal
σ_sq 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv Real Complex Real.instCommSemiring Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Complex.instRCLike EquivLike.toFunLike ContinuousAlgEquiv.equivLike σ	—	RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd

---

← Back to Index