DiscreteValuativeRel

📁 Source: Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean

Statistics

Metric	Count
Definitions	0
Theorems of_compatible_withZeroMulInt, nonempty_orderIso_withZeroMul_int_iff	2
Total	2

ValuativeRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_orderIso_withZeroMul_int_iff 📖	mathematical	—	OrderMonoidIso ValueGroupWithZero WithZero Multiplicative PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderValueGroupWithZero WithZero.instPreorder Multiplicative.preorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instMulValueGroupWithZero MulZeroClass.toMul WithZero.instMulZeroClass Multiplicative.mul IsDiscrete IsNontrivial MulArchimedean CommMonoidWithZero.toCommMonoid instCommMonoidWithZeroValueGroupWithZero	—	map_inv₀ MulEquivClass.toMonoidWithZeroHomClass OrderMonoidIso.instMulEquivClass EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass OrderMonoidIso.instOrderIsoClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Int.instZeroLEOneClass eq_or_ne map_inv_le_iff WithZero.log_le_log le_of_not_gt 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 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero 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 WithZero.log_lt_log NeZero.one WithZero.instNontrivial map_inv_lt_iff LT.lt.ne MulArchimedean.comap WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt OrderMonoidIso.strictMono LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered isNontrivial_iff_nontrivial_units IsDiscrete.has_maximal_element exists_between LT.lt.not_ge

ValuativeRel.IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_compatible_withZeroMulInt 📖	mathematical	—	ValuativeRel.IsDiscrete	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt Set.Nontrivial.not_subsingleton MonoidWithZeroHom.range_nontrivial WithZero.instNontrivial WithZero.denselyOrdered_set_iff_subsingleton StrictMono.denselyOrdered_range ValuativeRel.ValueGroupWithZero.embed_strictMono ValuativeRel.nonempty_orderIso_withZeroMul_int_iff LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered ValuativeRel.isNontrivial_iff_nontrivial_units ValuativeRel.instMulArchimedeanValueGroupWithZeroOfIsRankLeOne zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Contrapose.contrapose₁ LT.lt.ne' Units.val_le_val Eq.le

---

← Back to Index