Commit 2024-11-08 15:45 02e7451a

View on Github →

refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting (#17708) Instead of using Submodule.map₂ (which doesn't apply in the noncommutative setting), redefine the Mul and SMul to be defeq to AddSubmonoid.mul. In general, if a semiring A is a module over a semiring R such that IsScalarTower R A A is true, then the product of a Submodule R A with a Set A will be a Submodule R A, but we do not need this heterogeneous multiplication yet. We mainly intend to apply this to the case A = R.

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.mul_eq_map₂

modified theorem Submodule.mul_eq_span_mul_set

added theorem Submodule.pow_eq_npowRec

modified theorem Submodule.restrictScalars_mul

modified theorem Submodule.span_mul_span

Modified Mathlib/Algebra/Group/Defs.lean

added theorem npowRec_add

added theorem npowRec_succ

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Finiteness.lean

modified theorem Submodule.FG.mul

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.mul_eq_bot

modified theorem Ideal.one_eq_top

modified theorem Ideal.pow_right_mono

modified theorem Ideal.sup_pow_add_le_pow_sup_pow

added theorem Submodule.smul_eq_map₂

modified theorem Submodule.smul_le

added theorem Submodule.smul_toAddSubmonoid

modified theorem Submodule.span_smul_span

Modified Mathlib/RingTheory/Kaehler/Basic.lean