Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-11 16:08 d8531745

View on Github →

feat(ring_theory/derivation): The kernel of the map S ⊗[R] S →ₐ[R] S. (#15856)

Estimated changes

Modified src/ring_theory/derivation.lean

added def derivation.llcomp

added def derivation.tensor_product_to

added theorem derivation.tensor_product_to_mul

added theorem derivation.tensor_product_to_tmul

added def derivation_module.ideal

added theorem derivation_module.one_smul_sub_smul_one_mem_ideal

added theorem derivation_module.span_range_eq_ideal

added theorem derivation_module.submodule_span_range_eq_ideal