Def AddHom.mulLeft

Modification history

2023-09-12 12:40

Mathlib/Algebra/Ring/Basic.lean

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

Modified AddHom.mulLeft View on Github →

2022-12-04 13:00

Mathlib/Algebra/Ring/Basic.lean

feat: port algebra.ring.basic (#830) …

Added AddHom.mulLeft View on Github →