algebraMapSubmonoid_powers — Mathlib

English

The image of the submonoid of powers under the algebra map equals the powers submonoid of the image: Algebra.algebraMapSubmonoid S (.powers r) = Submonoid.powers (algebraMap R S r).

Русский

Образ подмоноида степеней через алгебраическое отображение равен подмоноиду степеней образа.

LaTeX

$$Algebra.algebraMapSubmonoid S (Submonoid.powers r) = Submonoid.powers (algebraMap R S r)$$

Lean4

@[simp]
theorem algebraMapSubmonoid_powers {S : Type*} [Semiring S] [Algebra R S] (r : R) :
    Algebra.algebraMapSubmonoid S (.powers r) = Submonoid.powers (algebraMap R S r) := by
  simp [Algebra.algebraMapSubmonoid]

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