Documentation Verification Report

Equivalence

📁 Source: Mathlib/Analysis/AbsoluteValue/Equivalence.lean

Statistics

Metric	Count
Definitions `IsEquiv`, `instSetoid`	2
Theorems `eq_iff_eq`, `eq_one_iff`, `equivWithAbs_image_mem_nhds_zero`, `isEmbedding_equivWithAbs`, `isNontrivial`, `isNontrivial_congr`, `le_iff_le`, `le_one_iff`, `log_div_log_eq_log_div_log`, `log_div_log_pos`, `lt_iff_lt`, `lt_one_iff`, `one_le_iff`, `one_lt_iff`, `refl`, `rfl`, `trans`, `eq_trivial_of_isEquiv_trivial`, `exists_lt_one_one_le_of_not_isEquiv`, `exists_one_lt_lt_one_of_not_isEquiv`, `exists_one_lt_lt_one_pi_of_not_isEquiv`, `isEquiv_iff_exists_rpow_eq`, `isEquiv_iff_isHomeomorph`, `isEquiv_iff_lt_one_iff`, `isEquiv_of_lt_one_imp`, `isEquiv_refl`, `isEquiv_symm`, `isEquiv_trans`, `isEquiv_trivial_iff_eq_trivial`	29
Total	31

AbsoluteValue

Definitions

Name	Category	Theorems
`IsEquiv` 📖	MathDef	16 math math: `NumberField.InfinitePlace.eq_iff_isEquiv`, `isEquiv_trivial_iff_eq_trivial`, `IsEquiv.rfl`, `isEquiv_refl`, `isEquiv_iff_lt_one_iff`, `Rat.AbsoluteValue.equiv_real_of_unbounded`, `Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv`, `Rat.AbsoluteValue.equiv_on_nat_iff_equiv`, `isEquiv_of_lt_one_imp`, `IsEquiv.refl`, `Rat.AbsoluteValue.not_real_equiv_padic`, `Rat.AbsoluteValue.equiv_padic_of_bounded`, `Rat.AbsoluteValue.not_real_isEquiv_padic`, `isEquiv_iff_exists_rpow_eq`, `isEquiv_iff_isHomeomorph`, `eq_trivial_of_isEquiv_trivial`
`instSetoid` 📖	CompOp	1 math math: `Rat.AbsoluteValue.equiv_real_or_padic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_trivial_of_isEquiv_trivial` 📖	mathematical	—	`IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `trivial` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `IsStrictOrderedRing.toCharZero`	—	`isEquiv_trivial_iff_eq_trivial`
`exists_lt_one_one_le_of_not_isEquiv` 📖	mathematical	`IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Preorder.toLE`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `isEquiv_of_lt_one_imp`
`exists_one_lt_lt_one_of_not_isEquiv` 📖	mathematical	`IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`exists_lt_one_one_le_of_not_isEquiv` `IsEquiv.symm` `map_div₀` `monoidWithZeroHomClass` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `pos_iff` `lt_of_lt_of_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `lt_of_le_of_lt'`
`exists_one_lt_lt_one_pi_of_not_isEquiv` 📖	mathematical	`IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pairwise` `IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`Fintype.induction_subsingleton_or_nontrivial` `IsNontrivial.exists_abv_gt_one` `AddGroup.existsAddOfLE` `eq_or_ne` `Nat.card_eq_two_iff'` `Fintype.card_eq_nat_card` `exists_one_lt_lt_one_of_not_isEquiv` `Fintype.one_lt_card_iff_nontrivial` `exists_ne` `Fintype.card_subtype_lt` `Pairwise.comp_of_injective` `Subtype.val_injective` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `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` `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.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `sub_eq_zero_of_eq` `Fintype.card_subtype_eq_or_eq_of_ne` `Subtype.finite` `Finite.of_fintype` `Ne.lt_or_gt`
`isEquiv_iff_exists_rpow_eq` 📖	mathematical	—	`IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder` `Real.instLT` `Real.instZero` `Real.instPow` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`IsEquiv.log_div_log_pos` `eq_or_ne` `map_zero` `Real.zero_rpow` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `IsEquiv.eq_one_iff` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Real.one_rpow` `IsEquiv.log_div_log_eq_log_div_log` `IsEquiv.symm` `div_eq_inv_mul` `Real.rpow_mul` `nonneg` `Real.rpow_inv_log` `pos` `Iff.not` `Real.exp_one_rpow` `Real.exp_log` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Real.rpow_one` `not_isNontrivial_apply` `IsEquiv.isNontrivial_congr` `isEquiv_iff_lt_one_iff` `Real.instIsStrictOrderedRing` `Real.rpow_lt_one_iff'`
`isEquiv_iff_isHomeomorph` 📖	mathematical	—	`IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder` `IsHomeomorph` `WithAbs` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithAbs.normedField` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs.instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `WithAbs.equivWithAbs`	—	`isHomeomorph_iff_isEmbedding_surjective` `IsEquiv.isEmbedding_equivWithAbs` `RingEquiv.surjective` `isEquiv_iff_lt_one_iff` `Real.instIsStrictOrderedRing` `RingEquiv.apply_symm_apply` `NormedDivisionRing.toNormMulClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Filter.Tendsto.comp` `Continuous.tendsto` `Topology.IsEmbedding.continuous` `Topology.IsEmbedding.continuous_iff` `continuous_id`
`isEquiv_iff_lt_one_iff` 📖	mathematical	—	`IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`IsEquiv.lt_one_iff` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `eq_or_ne` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `monoidWithZeroHomClass` `map_zero` `nonnegHomClass` `le_iff_le_iff_lt_iff_lt` `one_mul` `mul_inv_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `map_inv₀` `map_mul` `mulHomClass`
`isEquiv_of_lt_one_imp` 📖	mathematical	`IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`IsEquiv`	—	`isEquiv_iff_lt_one_iff` `eq_or_ne` `map_zero` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IsNontrivial.exists_abv_lt_one` `one_mul` `mul_inv_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `monoidWithZeroHomClass` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_inv₀` `map_mul` `mulHomClass` `lt_of_lt_of_le` `one_le_pow₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `exists_pow_lt_of_lt_one` `pos` `not_le` `not_lt` `LT.lt.le`
`isEquiv_refl` 📖	mathematical	—	`IsEquiv`	—	`IsEquiv.refl`
`isEquiv_symm` 📖	—	`IsEquiv`	—	—	`IsEquiv.symm`
`isEquiv_trans` 📖	—	`IsEquiv`	—	—	`IsEquiv.trans`
`isEquiv_trivial_iff_eq_trivial` 📖	mathematical	—	`IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `trivial` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `IsStrictOrderedRing.toCharZero`	—	`IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `ext` `IsEquiv.eq_one_iff` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_zero` `IsEquiv.rfl`

AbsoluteValue.IsEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff_eq` 📖	mathematical	`AbsoluteValue.IsEquiv`	`DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	—
`eq_one_iff` 📖	mathematical	`AbsoluteValue.IsEquiv`	`DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `eq_iff_eq`
`equivWithAbs_image_mem_nhds_zero` 📖	mathematical	`AbsoluteValue.IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder` `Set` `WithAbs` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithAbs.normedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	`Set.image` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs.instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `WithAbs.equivWithAbs`	—	`Metric.mem_nhds_iff` `AbsoluteValue.isEquiv_iff_exists_rpow_eq` `Real.rpow_pos_of_pos` `RingEquiv.apply_symm_apply` `Set.mem_image_of_mem` `dist_zero_right` `Real.rpow_lt_rpow_iff` `AbsoluteValue.nonneg` `LT.lt.le` `WithAbs.norm_eq_abv` `Metric.mem_ball`
`isEmbedding_equivWithAbs` 📖	mathematical	`AbsoluteValue.IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder`	`Topology.IsEmbedding` `WithAbs` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithAbs.normedField` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs.instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `WithAbs.equivWithAbs`	—	`Topology.IsInducing.isEmbedding` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `IsTopologicalAddGroup.isInducing_iff_nhds_zero` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomClass.toAddMonoidHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Filter.ext` `equivWithAbs_image_mem_nhds_zero` `RingEquiv.image_eq_preimage_symm` `Set.preimage_preimage` `RingEquiv.symm_apply_apply` `Set.instReflSubset` `Filter.mem_map_iff_exists_image` `Filter.map_equiv_symm` `RingEquiv.coe_toEquiv` `Filter.mem_of_superset` `symm` `WithAbs.equivWithAbs_symm` `RingEquiv.coe_toEquiv_symm`
`isNontrivial` 📖	—	`AbsoluteValue.IsEquiv` `AbsoluteValue.IsNontrivial`	—	—	`isNontrivial_congr`
`isNontrivial_congr` 📖	mathematical	`AbsoluteValue.IsEquiv`	`AbsoluteValue.IsNontrivial`	—	`not_iff_not` `eq_one_iff`
`le_iff_le` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	—
`le_one_iff` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass`
`log_div_log_eq_log_div_log` 📖	mathematical	`AbsoluteValue.IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`one_lt_iff` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `exists_rat_btwn` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `div_lt_div_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.log_pos` `mul_comm` `not_lt_of_gt` `lt_one_iff` `map_div₀` `AbsoluteValue.monoidWithZeroHomClass` `map_zpow₀` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `div_lt_one` `zpow_pos` `Real.instZeroLEOneClass` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.log_lt_log_iff` `pow_pos` `Real.log_zpow` `Real.log_pow` `Real.instNontrivial` `Rat.cast_natCast` `Rat.cast_intCast` `Rat.cast_div` `RCLike.charZero_rclike` `Rat.num_div_den` `one_lt_div` `lt_of_le_of_ne` `inv_ne_zero` `map_inv₀` `Real.log_inv` `neg_div_neg_eq` `one_lt_inv_iff₀` `AbsoluteValue.pos` `Ne.lt_of_le`
`log_div_log_pos` 📖	mathematical	`AbsoluteValue.IsEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.semiring` `Real.partialOrder`	`Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`Ne.lt_or_gt` `neg_div_neg_eq` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `neg_pos_of_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.log_neg` `AbsoluteValue.pos` `lt_one_iff` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Real.log_pos` `one_lt_iff`
`lt_iff_lt` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`lt_iff_lt_of_le_iff_le'`
`lt_one_iff` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `lt_iff_lt`
`one_le_iff` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass`
`one_lt_iff` 📖	mathematical	`AbsoluteValue.IsEquiv`	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `lt_iff_lt`
`refl` 📖	mathematical	—	`AbsoluteValue.IsEquiv`	—	—
`rfl` 📖	mathematical	—	`AbsoluteValue.IsEquiv`	—	—
`trans` 📖	—	`AbsoluteValue.IsEquiv`	—	—	—

---

← Back to Index