Metric

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

Statistics

Metric	Count
Definitions `center`, `instDist`, `instMetricSpace`, `metricSpaceAux`	4
Theorems `center_im`, `center_re`, `center_zero`, `cmp_dist_eq_cmp_dist_coe_center`, `cosh_dist`, `cosh_dist'`, `cosh_half_dist`, `dist_center_dist`, `dist_coe_center`, `dist_coe_center_sq`, `dist_coe_le`, `dist_comm`, `dist_eq`, `dist_eq_iff_dist_coe_center_eq`, `dist_eq_iff_eq_sinh`, `dist_eq_iff_eq_sq_sinh`, `dist_le_dist_coe_div_sqrt`, `dist_le_iff_dist_coe_center_le`, `dist_le_iff_le_sinh`, `dist_log_im_le`, `dist_lt_iff_dist_coe_center_lt`, `dist_of_re_eq`, `dist_self_center`, `dist_triangle`, `exp_half_dist`, `im_div_exp_dist_le`, `im_le_im_mul_exp_dist`, `im_pos_of_dist_center_le`, `image_coe_ball`, `image_coe_closedBall`, `image_coe_sphere`, `instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal`, `instProperSpace`, `isometry_pos_mul`, `isometry_real_vadd`, `isometry_vertical_line`, `le_dist_coe`, `le_dist_iff_le_dist_coe_center`, `lt_dist_iff_lt_dist_coe_center`, `sinh_half_dist`, `sinh_half_dist_add_dist`, `tanh_half_dist`	42
Total	46

UpperHalfPlane

Definitions

Name	Category	Theorems
`center` 📖	CompOp	16 math math: `image_coe_sphere`, `dist_le_iff_dist_coe_center_le`, `center_zero`, `center_re`, `image_coe_ball`, `center_im`, `image_coe_closedBall`, `dist_coe_center`, `lt_dist_iff_lt_dist_coe_center`, `dist_lt_iff_dist_coe_center_lt`, `dist_self_center`, `dist_eq_iff_dist_coe_center_eq`, `cmp_dist_eq_cmp_dist_coe_center`, `le_dist_iff_le_dist_coe_center`, `dist_center_dist`, `dist_coe_center_sq`
`instDist` 📖	CompOp	29 math math: `im_div_exp_dist_le`, `dist_le_iff_dist_coe_center_le`, `dist_eq_iff_eq_sinh`, `dist_log_im_le`, `im_le_im_mul_exp_dist`, `dist_eq_iff_eq_sq_sinh`, `dist_triangle`, `dist_of_re_eq`, `cosh_dist`, `dist_coe_center`, `lt_dist_iff_lt_dist_coe_center`, `dist_lt_iff_dist_coe_center_lt`, `dist_eq`, `dist_eq_iff_dist_coe_center_eq`, `cmp_dist_eq_cmp_dist_coe_center`, `le_dist_coe`, `le_dist_iff_le_dist_coe_center`, `dist_comm`, `dist_center_dist`, `dist_le_dist_coe_div_sqrt`, `cosh_half_dist`, `exp_half_dist`, `sinh_half_dist_add_dist`, `dist_coe_le`, `sinh_half_dist`, `dist_le_iff_le_sinh`, `dist_coe_center_sq`, `cosh_dist'`, `tanh_half_dist`
`instMetricSpace` 📖	CompOp	8 math math: `image_coe_sphere`, `isometry_real_vadd`, `isometry_vertical_line`, `image_coe_ball`, `image_coe_closedBall`, `instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal`, `instProperSpace`, `isometry_pos_mul`
`metricSpaceAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_im` 📖	mathematical	—	`im` `center` `Real` `Real.instMul` `Real.cosh`	—	—
`center_re` 📖	mathematical	—	`re` `center`	—	—
`center_zero` 📖	mathematical	—	`center` `Real` `Real.instZero`	—	`ext_re_im` `Real.cosh_zero` `mul_one`
`cmp_dist_eq_cmp_dist_coe_center` 📖	mathematical	—	`cmp` `Real` `Real.instLT` `Real.decidableLT` `Dist.dist` `UpperHalfPlane` `instDist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.instMul` `im` `Real.sinh`	—	`lt_or_ge` `LT.lt.cmp_eq_gt` `LT.lt.trans_le` `dist_nonneg` `mul_neg_of_pos_of_neg` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `Real.sinh_neg_iff` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Mathlib.Meta.Positivity.sinh_nonneg_of_nonneg` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `StrictMonoOn.cmp_map_eq` `Real.cosh_strictMonoOn` `pow_left_strictMonoOn₀` `IsOrderedRing.toMulPosMono` `two_ne_zero` `cmp.congr_simp` `dist_coe_center_sq` `cmp_mul_pos_left` `cmp_sub_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_sub` `cmp_add_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `zero_add`
`cosh_dist` 📖	mathematical	—	`Real.cosh` `Dist.dist` `UpperHalfPlane` `instDist` `Real` `Real.instAdd` `Real.instOne` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_eq` `Real.cosh_two_mul` `Real.cosh_sq'` `add_assoc` `two_mul` `Real.sinh_arsinh` `div_pow` `mul_pow` `Real.sq_sqrt` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `sq` `mul_assoc` `mul_div_assoc` `mul_div_mul_left` `ne_of_gt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`cosh_dist'` 📖	mathematical	—	`Real.cosh` `Dist.dist` `UpperHalfPlane` `instDist` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `re` `im` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `cosh_dist` `Complex.sq_norm` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `ne_of_gt` `im_pos` `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.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `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.cast_pos` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_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.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow`
`cosh_half_dist` 📖	mathematical	—	`Real.cosh` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Dist.dist` `UpperHalfPlane` `instDist` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `Real.instMul` `Real.sqrt` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_of_lt` `Real.cosh_pos` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `dist_nonneg` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos` `im_pos` `Real.cosh_sq'` `sinh_half_dist` `div_pow` `one_add_div` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `mul_pow` `Real.sq_sqrt` `Complex.sq_norm` `Complex.normSq_sub` `Complex.normSq_conj` `Complex.conj_conj` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add`
`dist_center_dist` 📖	mathematical	—	`Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `UpperHalfPlane` `instDist` `Real` `Real.instMul` `im` `Real.sinh`	—	`dist_eq_iff_dist_coe_center_eq`
`dist_coe_center` 📖	mathematical	—	`Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.sqrt` `Real` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `im` `Real.instSub` `Real.cosh` `UpperHalfPlane` `instDist` `Monoid.toNatPow` `Real.instMonoid` `Real.sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.sqrt_sq` `dist_nonneg` `dist_coe_center_sq`
`dist_coe_center_sq` 📖	mathematical	—	`Real` `Monoid.toNatPow` `Real.instMonoid` `Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `im` `Real.instSub` `Real.cosh` `UpperHalfPlane` `instDist` `Real.sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `ne_of_gt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `im_pos` `Complex.sq_norm` `sub_sq` `mul_pow` `Real.cosh_sq` `cosh_dist'` `mul_sub` `mul_div_cancel₀` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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_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.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.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.mul_congr` `Nat.cast_one`
`dist_coe_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `im` `Real.instSub` `Real.exp` `UpperHalfPlane` `instDist` `Real.instOne`	—	`dist_triangle_right` `dist_center_dist` `dist_self_center` `mul_add` `Distrib.leftDistribClass` `add_sub_assoc` `Real.sinh_add_cosh`
`dist_comm` 📖	mathematical	—	`Dist.dist` `UpperHalfPlane` `instDist`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `mul_comm`
`dist_eq` 📖	mathematical	—	`Dist.dist` `UpperHalfPlane` `instDist` `Real` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.arsinh` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.sqrt` `im`	—	—
`dist_eq_iff_dist_coe_center_eq` 📖	mathematical	—	`Dist.dist` `UpperHalfPlane` `instDist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real` `Real.instMul` `im` `Real.sinh`	—	`eq_iff_eq_of_cmp_eq_cmp` `cmp_dist_eq_cmp_dist_coe_center`
`dist_eq_iff_eq_sinh` 📖	mathematical	—	`Dist.dist` `UpperHalfPlane` `instDist` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.sqrt` `im` `Real.sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `div_left_inj'` `two_ne_zero'` `CharZero.NeZero.two` `RCLike.charZero_rclike` `sinh_half_dist`
`dist_eq_iff_eq_sq_sinh` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Dist.dist` `UpperHalfPlane` `instDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `im` `Real.sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_eq_iff_eq_sinh` `sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `dist_nonneg` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos` `im_pos` `Mathlib.Meta.Positivity.sinh_nonneg_of_nonneg` `div_pow` `mul_pow` `Real.sq_sqrt` `le_of_lt` `mul_assoc` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0`
`dist_le_dist_coe_div_sqrt` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `UpperHalfPlane` `instDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.sqrt` `Real.instMul` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_le_iff_le_sinh` `div_mul_eq_div_div_swap` `Real.self_le_sinh_iff` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `dist_nonneg` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos` `im_pos`
`dist_le_iff_dist_coe_center_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `UpperHalfPlane` `instDist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.instMul` `im` `Real.sinh`	—	`le_iff_le_of_cmp_eq_cmp` `cmp_dist_eq_cmp_dist_coe_center`
`dist_le_iff_le_sinh` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `UpperHalfPlane` `instDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.sqrt` `im` `Real.sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `div_le_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_two'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sinh_le_sinh` `sinh_half_dist`
`dist_log_im_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.pseudoMetricSpace` `Real.log` `im` `UpperHalfPlane` `instDist`	—	`im_pos` `dist_of_re_eq` `Nat.instAtLeastTwoHAddOfNat` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `sub_self` `zero_pow` `Nat.instCharZero` `zero_add` `Real.sqrt_sq_eq_abs` `Complex.abs_im_le_norm` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos`
`dist_lt_iff_dist_coe_center_lt` 📖	mathematical	—	`Real` `Real.instLT` `Dist.dist` `UpperHalfPlane` `instDist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.instMul` `im` `Real.sinh`	—	`lt_iff_lt_of_cmp_eq_cmp` `cmp_dist_eq_cmp_dist_coe_center`
`dist_of_re_eq` 📖	mathematical	`re`	`Dist.dist` `UpperHalfPlane` `instDist` `Real` `PseudoMetricSpace.toDist` `Real.pseudoMetricSpace` `Real.log` `im`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `dist_eq_iff_dist_coe_center_eq` `Real.dist_eq` `Real.abs_sinh` `Real.log_div` `im_ne_zero` `Nat.instAtLeastTwoHAddOfNat` `Real.sinh_log` `Complex.dist_of_re_eq` `coe_im` `center_im` `Real.cosh_abs` `Real.cosh_log` `inv_div` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instIsOrderedRing` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `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'_ofNat` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`dist_self_center` 📖	mathematical	—	`Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real` `Real.instMul` `im` `Real.instSub` `Real.cosh` `Real.instOne`	—	`Complex.dist_of_re_eq` `center_re` `dist_comm` `Real.dist_eq` `mul_sub` `mul_one` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_nonneg` `covariant_swap_add_of_covariant_add` `le_mul_of_one_le_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `im_pos` `Real.one_le_cosh`
`dist_triangle` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `UpperHalfPlane` `instDist` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_le_iff_le_sinh` `sinh_half_dist_add_dist` `div_mul_eq_div_div` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `dist_comm` `dist_pos` `Complex.conj_eq_iff_im` `im_ne_zero` `div_mul_eq_mul_div` `div_le_div_of_nonneg_right` `EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos` `im_pos`
`exp_half_dist` 📖	mathematical	—	`Real.exp` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Dist.dist` `UpperHalfPlane` `instDist` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instAdd` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `Real.instMul` `Real.sqrt` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.sinh_add_cosh` `sinh_half_dist` `cosh_half_dist` `add_div`
`im_div_exp_dist_le` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `im` `Real.exp` `Dist.dist` `UpperHalfPlane` `instDist`	—	`div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.exp_pos` `im_le_im_mul_exp_dist`
`im_le_im_mul_exp_dist` 📖	mathematical	—	`Real` `Real.instLE` `im` `Real.instMul` `Real.exp` `Dist.dist` `UpperHalfPlane` `instDist`	—	`div_le_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `Real.exp_log` `Real.exp_sub` `Real.exp_le_exp` `LE.le.trans` `le_abs_self` `dist_log_im_le`
`im_pos_of_dist_center_le` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center` `Real.instMul` `im` `Real.sinh`	`Real.instLT` `Real.instZero` `Complex.im`	—	`mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sinh_lt_cosh` `mul_sub` `sub_le_sub_left` `dist_comm` `sub_le_comm` `LE.le.trans` `le_abs_self` `Complex.abs_im_le_norm`
`image_coe_ball` 📖	mathematical	—	`Set.image` `UpperHalfPlane` `Complex` `coe` `Metric.ball` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `center` `Real` `Real.instMul` `im` `Real.sinh`	—	`Set.ext` `dist_lt_iff_dist_coe_center_lt` `CanLift.prf` `canLift` `im_pos_of_dist_center_le` `Metric.ball_subset_closedBall` `Set.mem_image_of_mem`
`image_coe_closedBall` 📖	mathematical	—	`Set.image` `UpperHalfPlane` `Complex` `coe` `Metric.closedBall` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `center` `Real` `Real.instMul` `im` `Real.sinh`	—	`Set.ext` `dist_le_iff_dist_coe_center_le` `CanLift.prf` `canLift` `im_pos_of_dist_center_le` `Set.mem_image_of_mem`
`image_coe_sphere` 📖	mathematical	—	`Set.image` `UpperHalfPlane` `Complex` `coe` `Metric.sphere` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `center` `Real` `Real.instMul` `im` `Real.sinh`	—	`Set.ext` `dist_eq_iff_dist_coe_center_eq` `CanLift.prf` `canLift` `im_pos_of_dist_center_le` `Metric.sphere_subset_closedBall` `Set.mem_image_of_mem`
`instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal` 📖	mathematical	—	`IsIsometricSMul` `Matrix.SpecialLinearGroup` `Fin.fintype` `Real` `Real.commRing` `UpperHalfPlane` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `SLAction` `Algebra.id` `CommRing.toCommSemiring`	—	`Isometry.of_dist_eq` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `im_pos` `Complex.norm_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ne_zero` `im_inv_neg_coe_pos` `modular_S_smul` `inv_neg` `Nat.instAtLeastTwoHAddOfNat` `dist_neg_neg` `NormedAddGroup.to_isIsometricVAdd_left` `NormedAddGroup.to_isIsometricVAdd_right` `dist_inv_inv₀` `Complex.inv_im` `neg_div` `neg_neg` `div_mul_div_comm` `Real.sqrt_div` `mul_div` `div_div_div_comm` `norm_mul` `div_self` `div_one` `exists_SL2_smul_eq_of_apply_zero_one_eq_zero` `Isometry.comp` `isometry_real_vadd` `isometry_pos_mul` `exists_SL2_smul_eq_of_apply_zero_one_ne_zero`
`instProperSpace` 📖	mathematical	—	`ProperSpace` `UpperHalfPlane` `MetricSpace.toPseudoMetricSpace` `instMetricSpace`	—	`Topology.IsEmbedding.isCompact_iff` `isEmbedding_coe` `image_coe_closedBall` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace`
`isometry_pos_mul` 📖	mathematical	—	`Isometry` `UpperHalfPlane` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `Real` `Real.instLT` `Real.instZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Positive.instMonoidSubtypeLtOfNat` `Real.semiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `MulAction.toSemigroupAction` `posRealAction`	—	`Isometry.of_dist_eq` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `pos_real_im` `dist_smul₀` `NormedSpace.toNormSMulClass` `mul_mul_mul_comm` `Real.sqrt_mul` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sqrt_mul_self_eq_abs` `Real.norm_eq_abs` `mul_left_comm` `mul_div_mul_left` `abs_eq_zero` `covariant_swap_add_of_covariant_add` `LT.lt.ne'`
`isometry_real_vadd` 📖	mathematical	—	`Isometry` `UpperHalfPlane` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instMetricSpace` `HVAdd.hVAdd` `Real` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddAction.toAddSemigroupAction` `instAddActionReal`	—	`Isometry.of_dist_eq` `Nat.instAtLeastTwoHAddOfNat` `dist_add_left` `NormedAddGroup.to_isIsometricVAdd_left` `vadd_im`
`isometry_vertical_line` 📖	mathematical	—	`Isometry` `Real` `UpperHalfPlane` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `instMetricSpace` `Real.exp` `Real.exp_pos`	—	`Isometry.of_dist_eq` `Real.exp_pos` `dist_of_re_eq` `Real.log_exp`
`le_dist_coe` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMul` `im` `Real.instSub` `Real.instOne` `Real.exp` `Real.instNeg` `Dist.dist` `UpperHalfPlane` `instDist` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe`	—	`dist_center_dist` `dist_self_center` `Real.cosh_sub_sinh` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `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_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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_triangle`
`le_dist_iff_le_dist_coe_center` 📖	mathematical	—	`Real` `Real.instLT` `Dist.dist` `UpperHalfPlane` `instDist` `Real.instMul` `im` `Real.sinh` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center`	—	`lt_iff_lt_of_cmp_eq_cmp` `cmp_eq_cmp_symm` `cmp_dist_eq_cmp_dist_coe_center`
`lt_dist_iff_lt_dist_coe_center` 📖	mathematical	—	`Real` `Real.instLT` `Dist.dist` `UpperHalfPlane` `instDist` `Real.instMul` `im` `Real.sinh` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `center`	—	`lt_iff_lt_of_cmp_eq_cmp` `cmp_eq_cmp_symm` `cmp_dist_eq_cmp_dist_coe_center`
`sinh_half_dist` 📖	mathematical	—	`Real.sinh` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Dist.dist` `UpperHalfPlane` `instDist` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `Real.instMul` `Real.sqrt` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_eq` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Real.sinh_arsinh`
`sinh_half_dist_add_dist` 📖	mathematical	—	`Real.sinh` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Dist.dist` `UpperHalfPlane` `instDist` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `Real.sqrt` `im`	—	`Nat.instAtLeastTwoHAddOfNat` `add_div` `Real.sinh_add` `sinh_half_dist` `cosh_half_dist` `div_mul_div_comm` `Complex.dist_self_conj` `coe_im` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `im_pos` `mul_comm` `dist_comm` `Complex.dist_conj_comm` `mul_mul_mul_comm` `Real.sqrt_mul` `LT.lt.le` `Real.mul_self_sqrt`
`tanh_half_dist` 📖	mathematical	—	`Real.tanh` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Dist.dist` `UpperHalfPlane` `instDist` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.tanh_eq_sinh_div_cosh` `sinh_half_dist` `cosh_half_dist` `div_div_div_comm` `div_self` `ne_of_gt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.sqrt_pos_of_pos` `im_pos` `div_one`

---

← Back to Index