Commit 2024-02-25 10:47 46be2770

chore: split Ordered instances for subobjects into separate files (#10900) Moving these to separate files should make typeclass synthesis less expensive. Additionally two of them are quite long and this shrinks them slightly. This handles:

• Submonoid
• Subgroup
• Subsemiring
• Subring
• Subfield
• Submodule
• Subalgebra This also moves Units.posSubgroup into its own file. The copyright headers are from:
• https://github.com/leanprover-community/mathlib/pull/6489
• https://github.com/leanprover-community/mathlib/pull/8466