Def Units.coeHom

Modification history

2023-09-12 12:40

Mathlib/Algebra/Hom/Units.lean

chore: replace anonymous morphism constructors with named fields (#7015) …

Modified Units.coeHom View on Github →

2022-12-03 03:40

Mathlib/Algebra/Hom/Units.lean

feat: port Algebra.Hom.Units (#745) …

Added Units.coeHom View on Github →