Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-15 12:10 ad6d4764

View on Github →

refactor(ring_theory/derivation): remove old_structure_cmd (#9724)

Estimated changes

Modified src/geometry/manifold/derivation_bundle.lean

Modified src/ring_theory/derivation.lean

modified theorem derivation.mk_coe

deleted theorem derivation.to_fun_eq_coe