Theorem isAddLeftRegular_ofMul

Modification history

2025-11-18 16:33

Mathlib/Algebra/Group/TypeTags/Basic.lean

feat: characterise regular elements of type synonyms (#31739)

Added isAddLeftRegular_ofMul View on Github →