Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 05:24 91d9e963

View on Github →

chore(algebra/ring/basic): docs, simps (#4375)

  • add docstrings to all typeclasses in algebra/ring/basic;
  • add ring_hom.inhabited := ⟨id α⟩ to make linter happy;
  • given f : α →+* β, simplify f.to_monoid_hom and f.to_add_monoid_hom to coercions;
  • add simp lemmas for coercions of ring_hom.mk f _ _ _ _ to monoid_hom and add_monoid_hom.

Estimated changes

deleted theorem coe_add_monoid_hom
deleted theorem coe_monoid_hom
modified theorem ring_hom.to_fun_eq_coe