We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
simp
1 parent 609d880 commit b12383cCopy full SHA for b12383c
1 file changed
Mathlib/RingTheory/Derivation/DifferentialRing.lean
@@ -93,8 +93,4 @@ lemma DifferentialAlgebra.equiv {A : Type*} [CommRing A] [Differential A]
93
letI := Differential.equiv h.toRingEquiv
94
⟨fun a ↦ by
95
change (LinearMap.comp ..) _ = _
96
- simp only [RingHom.toAddMonoidHom_eq_coe,
97
- RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
98
- AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
99
- Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]
100
- apply h.symm.commutes⟩
+ simp [deriv_algebraMap]⟩
0 commit comments