Theorem RingHom.congr_fun

Modification history

2024-07-24 23:20

Mathlib/Algebra/Ring/Hom/Defs.lean

chore: protect `congr_arg`'s and `congr_fun`'s (#15083) …

Deleted RingHom.congr_fun View on Github →

2022-12-13 11:06

Mathlib/Algebra/Hom/Ring.lean

feat: Port `Algebra.Hom.Ring` (#958) …

Added RingHom.congr_fun View on Github →