nat_power_gradedMonoid — Mathlib

English

The powers p^i of a submodule p form a graded monoid under multiplication, with 1 in degree 0 and p^i · p^j ⊆ p^{i+j}.

Русский

Степени подмодуля p образуют градуированный моноид: 1 в нулевой степени, а p^i · p^j ⊆ p^{i+j}.

LaTeX

$$$$ SetLike.GradedMonoid\; (i \mapsto p^i) $$$$

Lean4

/-- A direct sum of powers of a submodule of an algebra has a multiplicative structure. -/
instance nat_power_gradedMonoid [CommSemiring S] [Semiring R] [Algebra S R] (p : Submodule S R) :
    SetLike.GradedMonoid fun i : ℕ => p ^ i
    where
  one_mem := by rw [← one_le, pow_zero]
  mul_mem i j p q hp
    hq := by
    rw [pow_add]
    exact Submodule.mul_mem_mul hp hq

Похожие утверждения