Commit 2025-06-22 09:31 36f34a44

View on Github →

chore: unprime the Prop-valued fields of Grp_Class (#26252) Follow up to #26102 From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

deleted theorem Grp_Class.left_inv

deleted theorem Grp_Class.right_inv

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean