Commit 2022-12-06 06:42 c6da265f

View on Github →

chore: copy norm_cast attributes in to_additive (#847)

Estimated changes

Modified Mathlib/Algebra/Group/Units.lean

Modified Mathlib/Tactic/ToAdditive.lean

modified def ToAdditive.copySimpAttribute