mathlib

d4f8a454 - feat(algebra/group/units): add decidability instance for `is_unit` (#14873)

feat(algebra/group/units): add decidability instance for `is_unit` (#14873) This adds a decidability instance for the `is_unit` predicate. See [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Decidability.20of.20.60is_unit.60.20on.20finite.20rings/near/286543269).