Mathlib v3 is deprecated. Go to Mathlib v4

Theorem derivation_module.one_smul_sub_smul_one_mem_ideal

Modification history

2022-08-17 14:53
src/ring_theory/derivation.lean
feat(ring_theory/derivation): Construction of the module of Kähler differentials. (#16047)
Deleted derivation_module.one_smul_sub_smul_one_mem_idealView on Github →
2022-08-11 16:08
src/ring_theory/derivation.lean
feat(ring_theory/derivation): The kernel of the map `S ⊗[R] S →ₐ[R] S`. (#15856)
Added derivation_module.one_smul_sub_smul_one_mem_idealView on Github →