Theorem Submodule.smul_induction_on'

Modification history

2024-12-04 12:33

Mathlib/Algebra/Algebra/Operations.lean

refactor: generalize `SMul (Ideal R) (Submodule R M)` to `SMul (Submodule R A) (Submodule R M)` (#18419) …

Modified Submodule.smul_induction_on'View on Github →

2023-03-09 08:23

Mathlib/RingTheory/Ideal/Operations.lean

feat: port RingTheory.Ideal.Operations (#2701)

Added Submodule.smul_induction_on'View on Github →