Commit 2024-02-28 17:59 449a4a9b

View on Github →

feat: ℕ, ℤ and ℚ≥0 are star-ordered rings (#10633) Also golf the existing instance for ℚ and rename Rat.num_nonneg_iff_zero_le to Rat.num_nonneg, Rat.num_pos_iff_pos to Rat.num_pos. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Algebra/Star/Order.lean

Created Mathlib/Data/Int/Star.lean

added theorem Int.addSubmonoid_closure_range_mul_self

added theorem Int.addSubmonoid_closure_range_pow

Modified Mathlib/Data/NNRat/Defs.lean

added theorem NNRat.«exists»

added theorem NNRat.«forall»

Modified Mathlib/Data/Rat/Order.lean

added theorem Rat.num_neg

modified theorem Rat.num_nonneg

added theorem Rat.num_nonpos

modified theorem Rat.num_pos

Modified Mathlib/Data/Rat/Star.lean

added theorem NNRat.addSubmonoid_closure_range_mul_self

added theorem NNRat.addSubmonoid_closure_range_pow

added theorem Rat.addSubmonoid_closure_range_mul_self

added theorem Rat.addSubmonoid_closure_range_pow

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem Subgroup.mk_eq_one

deleted theorem Subgroup.mk_eq_one_iff

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem Nat.addSubmonoid_closure_one

added theorem Submonoid.mk_eq_one

Modified Mathlib/MeasureTheory/Group/AddCircle.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean