Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit.op

Modification history

2023-05-24 15:42
src/algebra/group/opposite.lean
feat(algebra/group/opposite): `is_unit` lemmas for `mul_opposite` (#19080) …
Added is_unit.opView on Github →