Basic

📁 Source: Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Statistics

Metric	Count
Definitions `IsNontrivial`, `apply`, `abs`, `funLike`, `instInhabited`, `toMonoidHom`, `toMonoidWithZeroHom`, `toMulHom`, `trivial`, `IsAbsoluteValue`, `evalAbv`, `abvHom`, `abvHom'`, `toAbsoluteValue`	14
Theorems `exists_abv_gt_one`, `exists_abv_lt_one`, `abs_abv_sub_le_abv_sub`, `abs_apply`, `add_le`, `add_le'`, `apply_natAbs_eq`, `apply_nat_le_self`, `coe_mk`, `coe_toMonoidHom`, `coe_toMonoidWithZeroHom`, `coe_toMulHom`, `eq_on_nat_iff_eq_on_int`, `eq_zero`, `eq_zero'`, `ext`, `ext_iff`, `instMulRingNormClassOfNontrivialOfIsDomain`, `isAbsoluteValue`, `isNontrivial_iff_ne_trivial`, `le_add`, `le_sub`, `listSum_le`, `map_mul`, `map_neg`, `map_one`, `map_one_of_isLeftRegular`, `map_pow`, `map_sub`, `map_sub_eq_zero_iff`, `map_zero`, `monoidWithZeroHomClass`, `mulHomClass`, `ne_zero`, `ne_zero_iff`, `nonneg`, `nonneg'`, `nonnegHomClass`, `nonpos_iff`, `not_isNontrivial_apply`, `not_isNontrivial_iff`, `pos`, `pos_iff`, `sub_le`, `sub_le_add`, `subadditiveHomClass`, `trivial_apply`, `zeroHomClass`, `abs_abv_sub_le_abv_sub`, `abs_isAbsoluteValue`, `abv_add`, `abv_add'`, `abv_div`, `abv_eq_zero`, `abv_eq_zero'`, `abv_inv`, `abv_mul`, `abv_mul'`, `abv_neg`, `abv_nonneg`, `abv_nonneg'`, `abv_one`, `abv_one'`, `abv_pos`, `abv_pow`, `abv_sub`, `abv_sub_le`, `abv_zero`, `sub_abv_le_abv_sub`, `toAbsoluteValue_apply`	70
Total	84

AbsoluteValue

Definitions

Name	Category	Theorems
`IsNontrivial` 📖	MathDef	4 math math: `NumberField.InfinitePlace.isNontrivial`, `IsEquiv.isNontrivial_congr`, `not_isNontrivial_iff`, `isNontrivial_iff_ne_trivial`
`abs` 📖	CompOp	3 math math: `abs_isEuclidean`, `abs_apply`, `Rat.uniformSpace_eq`
`funLike` 📖	CompOp	129 math math: `map_neg`, `Polynomial.cardPowDegree_zero`, `Height.mulHeight₁_eq`, `Polynomial.exists_partition_polynomial`, `Padic.complete'`, `map_units_intCast`, `coe_mk`, `IsEuclidean.sub_mod_lt`, `IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one`, `eq_zero`, `abs_abv_sub_le_abv_sub`, `padicNormE.nonarchimedean'`, `Polynomial.exists_partition_polynomial_aux`, `padicNormE.image'`, `eq_on_nat_iff_eq_on_int`, `NumberField.InfinitePlace.coe_apply`, `padicNormE.eq_padic_norm'`, `isEquiv_iff_lt_one_iff`, `map_sub_eq_zero_iff`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv`, `apply_nat_le_self`, `Height.AdmissibleAbsValues.isNonarchimedean`, `IsEquiv.le_one_iff`, `Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv`, `Rat.AbsoluteValue.equiv_on_nat_iff_equiv`, `padicNormE.defn`, `padicNormE.add_eq_max_of_ne'`, `coe_toMonoidHom`, `Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one`, `abs_apply`, `Polynomial.gaussNorm_intAdicAbv_le_one`, `Polynomial.gaussNorm_lt_one_iff_contentIdeal_le`, `le_sub`, `IsEquiv.lt_iff_lt`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv`, `NumberField.InfinitePlace.smul_coe_apply`, `NumberField.place_apply`, `IsAbsoluteValue.toAbsoluteValue_apply`, `Padic.padicNormE.is_norm`, `IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one`, `Rat.AbsoluteValue.padic_eq_padicNorm`, `exists_one_lt_lt_one_pi_of_not_isEquiv`, `pos`, `IsEquiv.lt_one_iff`, `nonneg`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `pos_iff`, `IsEquiv.le_iff_le`, `IsEquiv.log_div_log_pos`, `Height.mulHeight_eq`, `NumberField.FinitePlace.coe_apply`, `map_units_int_smul`, `Height.AdmissibleAbsValues.mulSupport_finite`, `ext_iff`, `Polynomial.cardPowDegree_apply`, `Padic.complete''`, `MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply`, `Polynomial.exists_approx_polynomial`, `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one`, `WithAbs.norm_eq_abv`, `nonnegHomClass`, `trivial_apply`, `IsAdmissible.exists_approx`, `IsEuclidean.map_lt_map_iff'`, `IsEquiv.eq_iff_eq`, `nonpos_iff`, `monoidWithZeroHomClass`, `le_add`, `Padic.exi_rat_seq_conv`, `coe_toMulHom`, `IsAdmissible.exists_partition`, `not_isNontrivial_iff`, `MulRingNorm.mulRingNormEquivAbsoluteValue_apply`, `hasBasis_uniformity`, `IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff`, `exists_one_lt_lt_one_of_not_isEquiv`, `IsAdmissible.exists_partition'`, `Rat.AbsoluteValue.padic_le_one`, `sum_le`, `zeroHomClass`, `NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv`, `IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap`, `map_units_int`, `IsEquiv.one_lt_iff`, `IsEquiv.eq_one_iff`, `mulHomClass`, `map_pow`, `map_sub`, `map_prod`, `Padic.rat_dense'`, `not_isNontrivial_apply`, `Polynomial.cardPowDegree_nonzero`, `sub_le`, `Rat.AbsoluteValue.eq_on_nat_iff_eq`, `IsAdmissible.exists_approx_aux`, `Rat.AbsoluteValue.real_eq_abs`, `NumberField.toNNReal_valued_eq_adicAbv`, `add_le`, `instMulRingNormClassOfNontrivialOfIsDomain`, `subadditiveHomClass`, `IsEquiv.one_le_iff`, `IsEuclidean.map_lt_map_iff`, `IsNontrivial.exists_abv_lt_one`, `apply_natAbs_eq`, `isEquiv_iff_exists_rpow_eq`, `isAbsoluteValue`, `listSum_le`, `map_zero`, `map_mul`, `Height.AdmissibleAbsValues.product_formula`, `coe_toMonoidWithZeroHom`, `sub_le_add`, `IsNontrivial.exists_abv_gt_one`, `Rat.AbsoluteValue.apply_le_sum_digits`, `Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one`, `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max`, `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff`, `IsEquiv.log_div_log_eq_log_div_log`, `NumberField.FinitePlace.norm_def`, `NumberField.mixedEmbedding.convexBodySum_mem`, `exists_lt_one_one_le_of_not_isEquiv`, `ClassGroup.exists_mem_finset_approx'`, `Finset.max_abv_sum_one_le`, `ClassGroup.exists_mem_finsetApprox`, `map_one`, `IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk'`
`instInhabited` 📖	CompOp	—
`toMonoidHom` 📖	CompOp	1 math math: `coe_toMonoidHom`
`toMonoidWithZeroHom` 📖	CompOp	1 math math: `coe_toMonoidWithZeroHom`
`toMulHom` 📖	CompOp	4 math math: `coe_toMulHom`, `nonneg'`, `eq_zero'`, `add_le'`
`trivial` 📖	CompOp	3 math math: `isEquiv_trivial_iff_eq_trivial`, `trivial_apply`, `eq_trivial_of_isEquiv_trivial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_abv_sub_le_abv_sub` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike`	—	`abs_sub_le_iff` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_sub` `map_sub` `IsDomain.to_noZeroDivisors` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE`
`abs_apply` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `funLike` `abs` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—
`add_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`add_le'`
`add_le'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toMulHom` `Distrib.toAdd`	—	—
`apply_natAbs_eq` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddGroupWithOne.toIntCast`	—	`Int.cast_natCast` `Int.cast_neg` `map_neg`
`apply_nat_le_self` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`subsingleton_or_nontrivial` `Subsingleton.eq_zero` `map_zero` `Nat.cast_zero` `Nat.cast_succ` `le_imp_le_of_le_of_le` `add_le` `le_refl` `map_one` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`coe_mk` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd`	`DFunLike.coe` `AbsoluteValue` `funLike` `MulHom` `MulHom.funLike`	—	—
`coe_toMonoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `toMonoidHom` `AbsoluteValue` `funLike`	—	—
`coe_toMonoidWithZeroHom` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidWithZeroHom.funLike` `toMonoidWithZeroHom` `AbsoluteValue` `funLike`	—	—
`coe_toMulHom` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulHom.funLike` `toMulHom` `AbsoluteValue` `funLike`	—	—
`eq_on_nat_iff_eq_on_int` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddGroupWithOne.toIntCast`	—	`Int.cast_natCast` `Int.cast_neg` `map_neg`
`eq_zero` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eq_zero'`
`eq_zero'` 📖	mathematical	—	`MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toMulHom` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`ext` 📖	—	`DFunLike.coe` `AbsoluteValue` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike`	—	`ext`
`instMulRingNormClassOfNontrivialOfIsDomain` 📖	mathematical	—	`MulRingNormClass` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toNonAssocRing` `funLike`	—	`subadditiveHomClass` `monoidWithZeroHomClass` `ZeroHomClass.map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `map_neg` `MonoidWithZeroHomClass.toMonoidHomClass` `eq_zero`
`isAbsoluteValue` 📖	mathematical	—	`IsAbsoluteValue` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`nonneg` `eq_zero` `add_le` `map_mul`
`isNontrivial_iff_ne_trivial` 📖	mathematical	—	`IsNontrivial`	—	`trivial_apply` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `ext` `eq_or_ne` `map_zero`
`le_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_neg_cancel_right` `map_neg` `add_le`
`le_sub` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `funLike`	—	`sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `sub_add_cancel` `add_le`
`listSum_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`map_zero` `zeroHomClass` `LE.le.trans` `add_le` `add_le_add_right`
`map_mul` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`MulHom.map_mul'`
`map_neg` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_zero` `map_zero` `mul_self_eq_mul_self_iff` `map_mul` `neg_mul_neg` `LT.lt.ne'` `LT.lt.trans` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `pos` `neg_ne_zero`
`map_one` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_one_of_isLeftRegular` `IsRegular.left` `IsRegular.of_ne_zero` `IsDomain.toIsCancelMulZero` `ne_zero` `one_ne_zero` `NeZero.one`
`map_one_of_isLeftRegular` 📖	—	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`map_mul` `mul_one`
`map_pow` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`MonoidHom.map_pow`
`map_sub` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`neg_sub` `map_neg`
`map_sub_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eq_zero` `sub_eq_zero`
`map_zero` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eq_zero`
`monoidWithZeroHomClass` 📖	mathematical	—	`MonoidWithZeroHomClass` `AbsoluteValue` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `funLike`	—	`mulHomClass` `map_one` `map_zero`
`mulHomClass` 📖	mathematical	—	`MulHomClass` `AbsoluteValue` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `funLike`	—	`zeroHomClass` `MulHom.map_mul'`
`ne_zero` 📖	—	—	—	—	`ne_zero_iff`
`ne_zero_iff` 📖	—	—	—	—	`Iff.not` `eq_zero`
`nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`nonneg'`
`nonneg'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulHom.toFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `toMulHom`	—	—
`nonnegHomClass` 📖	mathematical	—	`NonnegHomClass` `AbsoluteValue` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `funLike`	—	`zeroHomClass` `nonneg'`
`nonpos_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `funLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eq_zero` `nonneg`
`not_isNontrivial_apply` 📖	mathematical	`IsNontrivial`	`DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`not_isNontrivial_iff`
`not_isNontrivial_iff` 📖	mathematical	—	`IsNontrivial` `DFunLike.coe` `AbsoluteValue` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Mathlib.Tactic.Push.not_and_eq`
`pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`pos_iff`
`pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `funLike`	—	`LE.le.lt_iff_ne'` `nonneg` `ne_zero_iff`
`sub_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`sub_eq_add_neg` `add_assoc` `neg_add_cancel_left` `add_le`
`sub_le_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`map_neg` `add_le`
`subadditiveHomClass` 📖	mathematical	—	`SubadditiveHomClass` `AbsoluteValue` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `funLike`	—	`zeroHomClass` `add_le'`
`trivial_apply` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `funLike` `trivial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`zeroHomClass` 📖	mathematical	—	`ZeroHomClass` `AbsoluteValue` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `funLike`	—	`eq_zero'`

AbsoluteValue.IsNontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_abv_gt_one` 📖	mathematical	`AbsoluteValue.IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`Ne.lt_or_gt` `map_inv₀` `AbsoluteValue.monoidWithZeroHomClass` `IsStrictOrderedRing.isDomain` `DivisionRing.toNontrivial` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `AbsoluteValue.pos`
`exists_abv_lt_one` 📖	mathematical	`AbsoluteValue.IsNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`exists_abv_gt_one` `AbsoluteValue.ne_zero_iff` `LT.lt.ne'` `LT.lt.trans` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `inv_ne_zero` `map_inv₀` `AbsoluteValue.monoidWithZeroHomClass` `IsStrictOrderedRing.isDomain` `DivisionRing.toNontrivial` `inv_lt_one₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `AbsoluteValue.pos`

AbsoluteValue.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

IsAbsoluteValue

Definitions

Name	Category	Theorems
`abvHom` 📖	CompOp	—
`abvHom'` 📖	CompOp	—
`toAbsoluteValue` 📖	CompOp	1 math math: `toAbsoluteValue_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_abv_sub_le_abv_sub` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`AbsoluteValue.abs_abv_sub_le_abv_sub`
`abs_isAbsoluteValue` 📖	mathematical	—	`IsAbsoluteValue` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`AbsoluteValue.isAbsoluteValue`
`abv_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`abv_add'`
`abv_add'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`abv_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`map_div₀` `MonoidWithZeroHom.monoidWithZeroHomClass` `instIsCancelMulZero` `GroupWithZero.toNontrivial`
`abv_eq_zero` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`abv_eq_zero'`
`abv_eq_zero'` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`abv_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`map_inv₀` `MonoidWithZeroHom.monoidWithZeroHomClass` `instIsCancelMulZero` `GroupWithZero.toNontrivial`
`abv_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`abv_mul'`
`abv_mul'` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`abv_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`AbsoluteValue.map_neg`
`abv_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`abv_nonneg'`
`abv_nonneg'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`abv_one` 📖	mathematical	—	`AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`AbsoluteValue.map_one`
`abv_one'` 📖	mathematical	—	`AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`AbsoluteValue.map_one_of_isLeftRegular` `IsRegular.left` `IsRegular.of_ne_zero` `AbsoluteValue.ne_zero` `one_ne_zero` `NeZero.one`
`abv_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`AbsoluteValue.pos_iff`
`abv_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`AbsoluteValue.map_pow`
`abv_sub` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`AbsoluteValue.map_sub`
`abv_sub_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_eq_add_neg` `add_assoc` `neg_add_cancel_left` `abv_add`
`abv_zero` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`AbsoluteValue.map_zero`
`sub_abv_le_abv_sub` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`AbsoluteValue.le_sub`
`toAbsoluteValue_apply` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `toAbsoluteValue`	—	—

IsAbsoluteValue.Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalAbv` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`IsAbsoluteValue` 📖	CompData	6 math math: `padicNorm.instIsAbsoluteValueRat`, `IsAbsoluteValue.abs_isAbsoluteValue`, `NormMulClass.isAbsoluteValue_norm`, `Padic.isAbsoluteValue`, `AbsoluteValue.isAbsoluteValue`, `Complex.isAbsoluteValueNorm`

---

← Back to Index