Documentation Verification Report

IsNonarchimedean

📁 Source: Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

Statistics

Metric	Count
Definitions `IsNonarchimedean`	1
Theorems `add_eq_left_of_lt`, `add_eq_max_of_ne`, `add_eq_right_of_lt`, `add_le`, `add_pow_le`, `apply_intCast_le_one_of_isNonarchimedean`, `apply_natCast_le_one_of_isNonarchimedean`, `apply_sum_le_sup_of_isNonarchimedean`, `finset_image_add`, `finset_image_add_of_nonempty`, `finset_powerset_image_add`, `multiset_image_add`, `multiset_image_add_of_nonempty`, `multiset_powerset_image_add`, `nmul_le`, `nsmul_le`	16
Total	17

IsNonarchimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_left_of_lt` 📖	—	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`LE.le.trans_eq` `max_eq_left_of_lt` `lt_irrefl` `add_neg_cancel_right` `max_self` `AddGroupSeminormClass.map_neg_eq_map` `max_lt` `lt_of_le_of_ne`
`add_eq_max_of_ne` 📖	mathematical	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Ne.lt_or_gt` `add_eq_right_of_lt` `max_eq_right_of_lt` `add_eq_left_of_lt` `max_eq_left_of_lt`
`add_eq_right_of_lt` 📖	—	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`LE.le.trans_eq` `max_eq_right_of_lt` `lt_irrefl` `neg_add_cancel_left` `max_self` `AddGroupSeminormClass.map_neg_eq_map` `max_lt` `lt_of_le_of_ne`
`add_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsNonarchimedean`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`le_trans` `max_le_iff` `le_add_iff_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `le_add_iff_nonneg_left` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add`
`add_pow_le` 📖	mathematical	`IsNonarchimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`finset_image_add` `le_trans` `mul_comm` `nmul_le` `SubmultiplicativeHomClass.map_mul_le_mul`
`apply_intCast_le_one_of_isNonarchimedean` 📖	mathematical	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Int.cast_natCast` `apply_natCast_le_one_of_isNonarchimedean` `AddGroupSeminormClass.toZeroHomClass` `AddGroupSeminormClass.toNonnegHomClass` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Int.cast_neg` `AddGroupSeminormClass.map_neg_eq_map`
`apply_natCast_le_one_of_isNonarchimedean` 📖	mathematical	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`nsmul_one` `map_one` `nsmul_le`
`apply_sum_le_sup_of_isNonarchimedean` 📖	mathematical	`IsNonarchimedean` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.Nonempty`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `Finset.sup'` `Lattice.toSemilatticeSup`	—	`Finset.Nonempty.cons_induction` `Finset.sum_singleton` `Finset.cons_nonempty` `Finset.sum_cons` `Finset.le_sup'_iff` `le_max_iff` `le_trans`
`finset_image_add` 📖	mathematical	`IsNonarchimedean` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe`	`Finset` `Finset.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum`	—	`multiset_image_add`
`finset_image_add_of_nonempty` 📖	mathematical	`IsNonarchimedean` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.Nonempty`	`Finset` `Finset.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum`	—	`multiset_image_add_of_nonempty`
`finset_powerset_image_add` 📖	mathematical	`IsNonarchimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.powersetCard` `Finset.card` `Finset.prod` `CommRing.toCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `SetLike.instMembership` `Finset.instSetLike`	—	`finset_image_add` `AddGroupSeminormClass.toZeroHomClass` `AddGroupSeminormClass.toNonnegHomClass` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Finset.powersetCard_nonempty`
`multiset_image_add` 📖	mathematical	`IsNonarchimedean` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe`	`Multiset` `Multiset.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiset.sum` `Multiset.map`	—	`Multiset.induction_on` `map_zero` `multiset_image_add_of_nonempty` `Multiset.cons_ne_zero`
`multiset_image_add_of_nonempty` 📖	mathematical	`IsNonarchimedean` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Multiset` `Multiset.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiset.sum` `Multiset.map`	—	`Multiset.induction_on` `Multiset.map_cons` `Multiset.sum_cons` `Multiset.map_congr` `add_zero` `le_max_iff` `le_trans`
`multiset_powerset_image_add` 📖	mathematical	`IsNonarchimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe`	`Multiset.card` `Multiset` `Multiset.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Multiset.map` `Multiset.prod` `CommRing.toCommMonoid` `Multiset.powersetCard`	—	`multiset_image_add` `AddGroupSeminormClass.toZeroHomClass` `AddGroupSeminormClass.toNonnegHomClass` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Multiset.mem_powersetCard` `Multiset.card_pos` `Nat.choose_pos` `Multiset.card_powersetCard` `Multiset.mem_of_le`
`nmul_le` 📖	mathematical	`IsNonarchimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`nsmul_eq_mul` `nsmul_le`
`nsmul_le` 📖	mathematical	`IsNonarchimedean` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DFunLike.coe`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul`	—	`zero_nsmul` `map_zero` `add_nsmul` `le_trans` `one_smul`

(root)

Definitions

Name	Category	Theorems
`IsNonarchimedean` 📖	MathDef	18 math math: `IsUltrametricDist.isNonarchimedean_norm`, `IsUltrametricDist.isNonarchimedean_invariantExtension`, `PadicAlgCl.isNonarchimedean`, `IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_norm`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv`, `Height.AdmissibleAbsValues.isNonarchimedean`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv`, `PadicComplex.isNonarchimedean`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef`, `isNonarchimedean_spectralNorm`, `IsUltrametricDist.algNormOfAlgEquiv_apply`, `Valued.isNonarchimedean_norm`, `IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef`, `isNonarchimedean_spectralNorm_of_finiteDimensional_normal`, `IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm`, `NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv`, `IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv`, `IsUltrametricDist.isNonarchimedean_nnnorm`

---

← Back to Index