English
Dependent induction principle for powers: to prove a property C(n,x) for x ∈ M^n, it suffices to verify base case at algebra map, and closedness under addition and multiplication by M.
Русский
Зависимый принцип индукции по степеням: чтобы доказать свойство C(n,x) для x ∈ M^n, достаточно проверить базовый случай и сохранение при сложении и умножении на M.
LaTeX
$$$\\text{pow\_induction\_on\_left'}\\; C : \\mathbb{N} \\to A \\to Prop \\Rightarrow \\cdots$$$
Lean4
/-- Sub-R-modules of an R-algebra form an idempotent semiring. -/
instance idemSemiring : IdemSemiring (Submodule R A)
where
__ := instNonUnitalSemiring
one_mul := Submodule.one_mul
mul_one := Submodule.mul_one
bot_le _ := bot_le
