Commit 2023-08-08 16:37 f6bf5e04

View on Github →

chore: fix names (Add)SubmonoidClass.Subtype (#6374)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

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

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

deleted def SubmonoidClass.Subtype

modified theorem SubmonoidClass.coe_subtype

added def SubmonoidClass.subtype

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/Subring/Basic.lean

Modified Mathlib/RingTheory/Subsemiring/Basic.lean