algebraMapSubmonoid_le_comap — Mathlib

English

For any f: A →ₐ[R] B, the inclusion algebraMapSubmonoid A M is contained in the comap of algebraMapSubmonoid B M along f.

Русский

Для любого f: A →ₐ[R] B выполняется включение algebraMapSubmonoid A M ≤ comap(f.toRingHom) (algebraMapSubmonoid B M).

LaTeX

$$$ algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom $$$

Lean4

theorem algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) :
    algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom :=
  by
  rw [← algebraMapSubmonoid_map_eq M f]
  exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)

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