Artie Khovanov

chore(Algebra/Order): deduplicate material on ordered algebras

6

--- [](https://gitpod.io/from-referrer/)

refactor(Algebra): generalise `support` from `Subsemiring` to `AddSubmonoid`

1

* Generalise `support(Add)Subgroup`, `support` and `HasIdealSupport` from `Subsemiring` to `(Add)Submonoid`, moving the material to a new file * Add documentation about supports * Renamed declarations were not deprecated as the...

refactor: Remove order instances from `SetLike`

1

* Remove order instances from `SetLike` * Add class `IsConcreteLE` for `SetLike` instances whose map is order-preserving See discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/563952738 --- [](https://gitpod.io/from-referrer/)

feat(Algebra): forgetful lemmas for `map` and `comap` on substructures

2

* Standardise the form of forgetful lemmas for `map` and `comap` (ie, `(co)map_toSubfoo`) * Add missing lemmas of this form * Mark all such lemmas as `simp` --- - [...