Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-20 15:11 593938cd

View on Github →

chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1062)

  • chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map From the perfectoid project.
  • Stupid error
  • Update src/ring_theory/algebra.lean Co-Authored-By: Chris Hughes [email protected]

Estimated changes