Modular

📁 Source: Mathlib/NumberTheory/Modular.lean

Statistics

Metric	Count
Definitions `term𝒟`, `«term𝒟ᵒ»`, `fd`, `fdo`, `lcRow0`, `lcRow0Extend`, `truncatedFundamentalDomain`	7
Theorems `abs_c_le_one`, `abs_two_mul_re_lt_one_of_mem_fdo`, `bottom_row_coprime`, `bottom_row_surj`, `c_eq_zero`, `coe_T_zpow_smul_eq`, `coe_truncatedFundamentalDomain`, `eq_smul_self_of_mem_fdo_mem_fdo`, `eq_zero_of_mem_fdo_of_T_zpow_mem_fdo`, `exists_eq_T_zpow_of_c_eq_zero`, `exists_max_im`, `exists_one_half_le_im_smul`, `exists_one_half_le_im_smul_and_norm_denom_le`, `exists_row_one_eq_and_min_re`, `exists_smul_mem_fd`, `g_eq_of_c_eq_one`, `im_T_inv_smul`, `im_T_smul`, `im_T_zpow_smul`, `im_lt_im_S_smul`, `isCompact_truncatedFundamentalDomain`, `lcRow0Extend_apply`, `lcRow0Extend_symm_apply`, `lcRow0_apply`, `normSq_S_smul_lt_one`, `one_lt_normSq_T_zpow_smul`, `re_T_inv_smul`, `re_T_smul`, `re_T_zpow_smul`, `smul_eq_lcRow0_add`, `tendsto_abs_re_smul`, `tendsto_lcRow0`, `tendsto_normSq_coprime_pair`, `three_le_four_mul_im_sq_of_mem_fd`, `three_lt_four_mul_im_sq_of_mem_fdo`	35
Total	42

Modular

Definitions

Name	Category	Theorems
`term𝒟` 📖	CompOp	—
`«term𝒟ᵒ»` 📖	CompOp	—

ModularGroup

Definitions

Name	Category	Theorems
`fd` 📖	CompOp	1 math math: `exists_smul_mem_fd`
`fdo` 📖	CompOp	—
`lcRow0` 📖	CompOp	3 math math: `tendsto_lcRow0`, `lcRow0_apply`, `smul_eq_lcRow0_add`
`lcRow0Extend` 📖	CompOp	2 math math: `lcRow0Extend_symm_apply`, `lcRow0Extend_apply`
`truncatedFundamentalDomain` 📖	CompOp	2 math math: `isCompact_truncatedFundamentalDomain`, `coe_truncatedFundamentalDomain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_c_le_one` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fdo` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	`abs` `instLatticeInt` `Int.instAddGroup` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `mul_lt_mul''` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `three_lt_four_mul_im_sq_of_mem_fdo` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `lt_of_le_of_ne'` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `Real.instZeroLEOneClass` `pow_four_le_pow_two_of_pow_two_le` `UpperHalfPlane.c_mul_im_sq_le_normSq_denom` `sq_nonneg` `IsOrderedRing.toPosMulMono` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `im_smul_eq_div_normSq` `div_pow` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `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_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `mul_pow` `le_of_not_gt` `Nat.cast_one` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Mathlib.Meta.NormNum.isNat_lt_true` `CancelDenoms.mul_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `eq_or_ne` `zero_pow` `Nat.instCharZero` `MulZeroClass.mul_zero` `abs_lt_of_sq_lt_sq'` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Int.cast_lt` `NeZero.charZero_one` `Int.cast_mul` `Int.cast_four` `Int.cast_three` `Int.cast_pow` `abs_one` `Int.instIsStrictOrderedRing` `sq_le_sq`
`abs_two_mul_re_lt_one_of_mem_fdo` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fdo`	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `UpperHalfPlane.re` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `abs_mul` `Real.instIsOrderedRing` `abs_two` `lt_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_two'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`bottom_row_coprime` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Matrix` `Matrix.det` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Matrix.SpecialLinearGroup.isCoprime_row`
`bottom_row_surj` 📖	mathematical	—	`Set.SurjOn` `Matrix.SpecialLinearGroup` `Fin.fintype` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Set.univ` `setOf` `IsCoprime` `CommRing.toCommSemiring`	—	`Matrix.det_fin_two` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `neg_mul` `sub_neg_eq_add` `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` `Set.mem_univ`
`c_eq_zero` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fdo` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	`Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`g_eq_of_c_eq_one` `neg_add_cancel` `zpow_zero` `one_mul` `normSq_S_smul_lt_one` `one_lt_normSq_T_zpow_smul` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Fintype.card_fin_two` `neg_eq_iff_eq_neg` `SL_neg_smul` `Int.abs_le_one_iff` `abs_c_le_one`
`coe_T_zpow_smul_eq` 📖	mathematical	—	`UpperHalfPlane.coe` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T` `Complex` `Complex.instAdd` `Complex.instIntCast`	—	`UpperHalfPlane.coe_specialLinearGroup_apply` `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`
`coe_truncatedFundamentalDomain` 📖	mathematical	—	`Set.image` `UpperHalfPlane` `Complex` `UpperHalfPlane.coe` `truncatedFundamentalDomain` `setOf` `Real` `Real.instLE` `Real.instZero` `Complex.im` `abs` `Real.lattice` `Real.instAddGroup` `Complex.re` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Norm.norm` `Complex.instNorm`	—	`Set.ext` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.le` `Complex.normSq_eq_norm_sq` `Real.instIsStrictOrderedRing` `abs_norm` `LE.le.lt_of_ne` `Mathlib.Tactic.Contrapose.contrapose₃` `sq_lt_one_iff₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `norm_nonneg` `zero_pow` `Nat.instCharZero` `add_zero` `LE.le.trans_lt` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo`
`eq_smul_self_of_mem_fdo_mem_fdo` 📖	—	`UpperHalfPlane` `Set` `Set.instMembership` `fdo` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	—	—	`exists_eq_T_zpow_of_c_eq_zero` `c_eq_zero` `eq_zero_of_mem_fdo_of_T_zpow_mem_fdo` `zpow_zero` `one_smul`
`eq_zero_of_mem_fdo_of_T_zpow_mem_fdo` 📖	—	`UpperHalfPlane` `Set` `Set.instMembership` `fdo` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T`	—	—	`Nat.instAtLeastTwoHAddOfNat` `abs_add'` `Real.instIsOrderedAddMonoid` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `re_T_zpow_smul` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Int.abs_lt_one_iff` `Int.cast_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Int.cast_one` `Int.cast_abs` `Real.instIsStrictOrderedRing`
`exists_eq_T_zpow_of_c_eq_zero` 📖	mathematical	`Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`Matrix.SpecialLinearGroup` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T`	—	`Matrix.SpecialLinearGroup.det_coe` `Matrix.det_fin_two` `Int.eq_one_or_neg_one_of_mul_eq_one'` `Matrix.SpecialLinearGroup.ext` `Fintype.complete` `coe_T_zpow` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Fintype.card_fin_two` `zpow_neg` `Matrix.adjugate_fin_two_of` `neg_zero` `neg_neg` `SL_neg_smul`
`exists_max_im` 📖	mathematical	—	`Real` `Real.instLE` `UpperHalfPlane.im` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing`	—	`isCoprime_one_left` `Filter.Tendsto.exists_within_forall_le` `tendsto_normSq_coprime_pair` `bottom_row_surj` `im_smul_eq_div_normSq` `div_le_div_iff_of_pos_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `UpperHalfPlane.im_pos` `UpperHalfPlane.normSq_denom_pos` `UpperHalfPlane.im_ne_zero` `bottom_row_coprime`
`exists_one_half_le_im_smul` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `UpperHalfPlane.im` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_smul_mem_fd` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `three_le_four_mul_im_sq_of_mem_fd` `UpperHalfPlane.im_pos` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`exists_one_half_le_im_smul_and_norm_denom_le` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `UpperHalfPlane.im` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `Norm.norm` `Complex` `Complex.instNorm` `UpperHalfPlane.denom` `DFunLike.coe` `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`	—	`Nat.instAtLeastTwoHAddOfNat` `le_total` `one_smul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `UpperHalfPlane.denom_one` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `LE.le.trans` `Real.instIsStrictOrderedRing` `abs_norm` `mul_le_iff_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `UpperHalfPlane.coe_im_pos` `Complex.normSq_eq_norm_sq` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `UpperHalfPlane.normSq_denom_pos` `UpperHalfPlane.im_ne_zero` `im_smul_eq_div_normSq` `exists_one_half_le_im_smul`
`exists_row_one_eq_and_min_re` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `UpperHalfPlane.re` `Matrix.SpecialLinearGroup` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing`	—	`Filter.Tendsto.exists_forall_le` `bottom_row_surj` `tendsto_abs_re_smul` `Set.mem_preimage` `Set.mem_singleton_iff`
`exists_smul_mem_fd` 📖	mathematical	—	`UpperHalfPlane` `Set` `Set.instMembership` `fd` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	—	`exists_max_im` `exists_row_one_eq_and_min_re` `bottom_row_coprime` `im_smul_eq_div_normSq` `denom_apply` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `SemigroupAction.mul_smul` `im_lt_im_S_smul` `Nat.instAtLeastTwoHAddOfNat` `abs_le` `Real.instIsOrderedAddMonoid` `T_mul_apply_one` `re_T_smul` `abs_cases` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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_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_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsRat.neg_to_eq` `Mathlib.Meta.NormNum.isRat_neg` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `CancelDenoms.sub_subst` `CancelDenoms.neg_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `sub_eq_zero_of_eq` `neg_eq_zero` `T_inv_mul_apply_one` `re_T_inv_smul` `Mathlib.Meta.NormNum.IsNNRat.to_eq`
`g_eq_of_c_eq_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` `S`	—	`Matrix.SpecialLinearGroup.det_coe` `Matrix.det_fin_two` `Matrix.eta_fin_two` `sub_eq_add_neg` `coe_T_zpow` `Matrix.mul_fin_two` `MulZeroClass.mul_zero` `mul_one` `zero_add` `one_mul` `add_zero` `MulZeroClass.zero_mul`
`im_T_inv_smul` 📖	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` `Matrix.SpecialLinearGroup.hasInv` `T`	—	`map_inv` `MonoidHom.instMonoidHomClass` `zpow_neg` `zpow_one` `im_T_zpow_smul`
`im_T_smul` 📖	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` `T`	—	`zpow_one` `im_T_zpow_smul`
`im_T_zpow_smul` 📖	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.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T`	—	`UpperHalfPlane.coe_im` `coe_T_zpow_smul_eq` `Complex.add_im` `Complex.intCast_im` `add_zero`
`im_lt_im_S_smul` 📖	mathematical	`Real` `Real.instLT` `DFunLike.coe` `MonoidWithZeroHom` `Complex` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `Real.semiring` `MonoidWithZeroHom.funLike` `Complex.normSq` `UpperHalfPlane.coe` `Real.instOne`	`UpperHalfPlane.im` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `S`	—	`im_smul_eq_div_normSq` `UpperHalfPlane.im_pos` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `UpperHalfPlane.normSq_pos` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `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.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_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.cast_one` `one_mul` `Int.cast_zero` `add_zero`
`isCompact_truncatedFundamentalDomain` 📖	mathematical	—	`IsCompact` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `truncatedFundamentalDomain`	—	`Topology.IsEmbedding.isCompact_iff` `UpperHalfPlane.isEmbedding_coe` `Nat.instAtLeastTwoHAddOfNat` `coe_truncatedFundamentalDomain` `Metric.isCompact_iff_isClosed_bounded` `Complex.instT2Space` `Complex.instProperSpace` `IsClosed.inter` `isClosed_le` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `continuous_const` `Complex.continuous_im` `Continuous.comp` `continuous_abs` `Real.instIsOrderedAddMonoid` `Complex.continuous_re` `continuous_norm` `Metric.isBounded_iff_subset_closedBall` `le_of_sq_le_sq` `Real.instIsStrictOrderedRing` `Real.sq_sqrt` `le_of_lt` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Complex.norm_eq_sqrt_sq_add_sq` `add_nonneg` `add_le_add` `covariant_swap_add_of_covariant_add` `sq_le_sq` `abs_of_pos` `one_half_pos` `sq_le_sq₀` `IsOrderedRing.toMulPosMono` `LE.le.trans` `Real.sqrt_pos_of_pos`
`lcRow0Extend_apply` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`DFunLike.coe` `LinearEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Real.instAddCommMonoid` `Matrix.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lcRow0Extend` `Pi.addCommMonoid` `Pi.Function.module` `Matrix.vecCons` `MulEquiv` `LinearMap.GeneralLinearGroup` `Units.instMul` `LinearMap` `Module.End.instMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MulEquiv.instEquivLike` `LinearMap.GeneralLinearGroup.generalLinearEquiv` `Matrix.GeneralLinearGroup` `Fin.fintype` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.GeneralLinearGroup.toLin` `Matrix.planeConformalMatrix` `Real.instField` `Real.instIntCast` `Real.instNeg` `LinearEquiv.refl` `Matrix.vecEmpty`	—	`RingHomInvPair.ids`
`lcRow0Extend_symm_apply` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`DFunLike.coe` `LinearEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `Real.instAddCommMonoid` `Matrix.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `lcRow0Extend` `Pi.addCommMonoid` `Pi.Function.module` `Matrix.vecCons` `MulEquiv` `LinearMap.GeneralLinearGroup` `Units.instMul` `LinearMap` `Module.End.instMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MulEquiv.instEquivLike` `LinearMap.GeneralLinearGroup.generalLinearEquiv` `Matrix.GeneralLinearGroup` `Fin.fintype` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.GeneralLinearGroup.toLin` `Matrix.planeConformalMatrix` `Real.instField` `Real.instIntCast` `Real.instNeg` `LinearEquiv.refl` `Matrix.vecEmpty`	—	`RingHomInvPair.ids`
`lcRow0_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `Real.instAddCommMonoid` `Matrix.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `LinearMap.instFunLike` `lcRow0` `Real.instAdd` `Real.instMul` `Real.instIntCast`	—	—
`normSq_S_smul_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `DFunLike.coe` `MonoidWithZeroHom` `Complex` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `Real.semiring` `MonoidWithZeroHom.funLike` `Complex.normSq` `UpperHalfPlane.coe`	`Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `S`	—	`UpperHalfPlane.coe_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` `map_div₀` `MonoidWithZeroHom.monoidWithZeroHomClass` `Complex.normSq_neg` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `one_div` `inv_one` `inv_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `UpperHalfPlane.normSq_pos` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`one_lt_normSq_T_zpow_smul` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fdo`	`Real` `Real.instLT` `Real.instOne` `DFunLike.coe` `MonoidWithZeroHom` `Complex` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `Real.semiring` `MonoidWithZeroHom.funLike` `Complex.normSq` `UpperHalfPlane.coe` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T`	—	`coe_T_zpow_smul_eq` `Nat.instAtLeastTwoHAddOfNat` `Int.nneg_mul_add_sq_of_abs_le_one` `Real.instIsStrictOrderedRing` `LT.lt.le` `abs_two_mul_re_lt_one_of_mem_fdo` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.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.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.cast_zero` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `add_zero`
`re_T_inv_smul` 📖	mathematical	—	`UpperHalfPlane.re` `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.hasInv` `T` `Real.instSub` `Real.instOne`	—	`map_inv` `MonoidHom.instMonoidHomClass` `zpow_neg` `zpow_one` `Int.cast_neg` `Int.cast_one` `re_T_zpow_smul`
`re_T_smul` 📖	mathematical	—	`UpperHalfPlane.re` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `T` `Real.instAdd` `Real.instOne`	—	`zpow_one` `Int.cast_one` `re_T_zpow_smul`
`re_T_zpow_smul` 📖	mathematical	—	`UpperHalfPlane.re` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `T` `Real.instAdd` `Real.instIntCast`	—	`UpperHalfPlane.coe_re` `coe_T_zpow_smul_eq` `Complex.add_re` `Complex.intCast_re`
`smul_eq_lcRow0_add` 📖	mathematical	`IsCoprime` `Int.instCommSemiring` `Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`UpperHalfPlane.coe` `Matrix.SpecialLinearGroup` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `Complex` `Complex.instAdd` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.ofReal` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `Real.instAddCommMonoid` `Matrix.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `LinearMap.instFunLike` `lcRow0` `Real.commRing` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Matrix.SpecialLinearGroup.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instIntCast` `Complex.instSub` `Complex.instMul`	—	`Nat.cast_zero` `Int.cast_zero` `Complex.instCharZero` `IsCoprime.sq_add_sq_ne_zero` `Int.instIsStrictOrderedRing` `IsCoprime.ne_zero` `Int.instNontrivial` `RCLike.charZero_rclike` `UpperHalfPlane.linear_ne_zero` `UpperHalfPlane.coe_specialLinearGroup_apply` `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` `Matrix.det_fin_two` `eq_intCast` `RingHom.instRingHomClass` `Complex.ofReal_add` `Complex.ofReal_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `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.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Matrix.SpecialLinearGroup.det_coe` `Int.cast_one` `Int.cast_sub` `Int.cast_mul` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.neg_congr` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Nat.cast_one` `Mathlib.Tactic.Ring.cast_zero`
`tendsto_abs_re_smul` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`Filter.Tendsto` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Real` `abs` `Real.lattice` `Real.instAddGroup` `UpperHalfPlane.re` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `Filter.cofinite` `Filter.atTop` `Real.instPreorder`	—	`inv_ne_zero` `Nat.cast_zero` `Int.cast_zero` `RCLike.charZero_rclike` `IsCoprime.sq_add_sq_ne_zero` `Int.instIsStrictOrderedRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsTopologicalSemiring.toContinuousAdd` `Int.cast_add` `Int.cast_pow` `Complex.ofReal_add` `Complex.ofReal_pow` `smul_eq_lcRow0_add` `Filter.Tendsto.comp` `Topology.IsClosedEmbedding.tendsto_cocompact` `Homeomorph.isClosedEmbedding` `tendsto_lcRow0` `tendsto_norm_cocompact_atTop` `instProperSpaceReal`
`tendsto_lcRow0` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`Filter.Tendsto` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Real` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `Real.instAddCommMonoid` `Matrix.module` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `LinearMap.instFunLike` `lcRow0` `Real.commRing` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Matrix.SpecialLinearGroup.monoid` `MonoidHom.instFunLike` `Matrix.SpecialLinearGroup.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Filter.cofinite` `Filter.cocompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`continuous_matrix` `Filter.Tendsto.of_tendsto_comp` `Filter.coprodᵢ_cofinite` `Finite.of_fintype` `Filter.coprodᵢ_cocompact` `Filter.Tendsto.pi_map_coprodᵢ` `Int.tendsto_coe_cofinite` `Filter.Tendsto.comp` `Function.Injective.tendsto_cofinite` `Subtype.coe_injective` `RingHomInvPair.ids` `Homeomorph.isClosedEmbedding` `instIsTopologicalAddGroupMatrix` `instIsTopologicalAddGroupReal` `instContinuousSMulMatrix` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instCompleteSpace` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Module.Finite.matrix` `Module.Free.self` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Matrix.ext` `Fintype.complete` `Int.cast_one` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one` `neg_neg` `Finset.sum_congr` `Fin.sum_univ_two` `Matrix.det_fin_two` `neg_mul` `Int.cast_sub` `Int.cast_mul` `neg_sub` `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.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Matrix.SpecialLinearGroup.det_coe` `Topology.IsClosedEmbedding.tendsto_cocompact` `Filter.comap_cocompact_le`
`tendsto_normSq_coprime_pair` 📖	mathematical	—	`Filter.Tendsto` `Real` `DFunLike.coe` `MonoidWithZeroHom` `Complex` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `Real.semiring` `MonoidWithZeroHom.funLike` `Complex.normSq` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `Filter.cofinite` `Filter.atTop` `Real.instPreorder`	—	`IsScalarTower.left` `mul_one` `Complex.ofReal_intCast` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Function.smulCommClass` `LinearMap.ext` `LT.lt.ne'` `UpperHalfPlane.coe_im_pos` `LinearMap.comp_apply` `LinearMap.smul_apply` `LinearMap.id_apply` `Fintype.complete` `Complex.add_im` `Complex.im_ofReal_mul` `Complex.ofReal_im` `add_zero` `mul_left_comm` `inv_mul_cancel₀` `map_add` `SemilinearMapClass.toAddHomClass` `Complex.instCharZero` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_add` `Distrib.leftDistribClass` `Complex.mul_conj` `Complex.conj_ofReal` `Complex.ofReal_mul` `zero_add` `inv_mul_eq_iff_eq_mul₀` `MulZeroClass.mul_zero` `LinearMap.ker_eq_bot_of_inverse` `RingHomInvPair.ids` `LinearMap.isClosedEmbedding_of_injective` `Real.instCompleteSpace` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Complex.instT2Space` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `Filter.coprodᵢ_cofinite` `Filter.coprodᵢ_cocompact` `Filter.Tendsto.pi_map_coprodᵢ` `Int.tendsto_coe_cofinite` `Filter.Tendsto.comp` `Complex.tendsto_normSq_cocompact_atTop` `Topology.IsClosedEmbedding.tendsto_cocompact`
`three_le_four_mul_im_sq_of_mem_fd` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fd`	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `UpperHalfPlane.im`	—	`abs_cases` `Real.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.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.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.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.le_of_le_of_eq` `Mathlib.Tactic.Linarith.mul_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.mul_eq` `neg_eq_zero` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Linarith.zero_mul_eq` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_of_lt`
`three_lt_four_mul_im_sq_of_mem_fdo` 📖	mathematical	`UpperHalfPlane` `Set` `Set.instMembership` `fdo`	`Real` `Real.instLT` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `UpperHalfPlane.im`	—	`abs_cases` `Real.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.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.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.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Linarith.mul_eq` `neg_eq_zero` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.mul_zero_eq` `Mathlib.Tactic.Linarith.mul_nonpos` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_of_lt` `Mathlib.Tactic.Linarith.zero_mul_eq` `mul_pos_of_neg_of_neg` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono`

---

← Back to Index