Commit 2024-09-01 19:15 5c196c69

View on Github →

chore(Algebra/Order/Monoid/Submonoid): Don't import GroupWithZero (#16381) Move Submonoid.pos to a new file Algebra.Order.GroupWithZero.Submonoid. Credit Chris for https://github.com/leanprover-community/mathlib3/pull/8466

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/GroupWithZero/Submonoid.lean

added theorem Submonoid.mem_pos

added def Submonoid.pos

Modified Mathlib/Algebra/Order/Monoid/Submonoid.lean

deleted theorem Submonoid.mem_pos

deleted def Submonoid.pos

Modified Mathlib/Algebra/Ring/Subring/Units.lean