pointwise_smul_eq_comap — Mathlib

English

For any a in M, a•S equals the comap of S under the opposite ring automorphism.

Русский

Для любого a в M, a•S равняется обратному образу S через противоположный кольцевой автоморфизм.

LaTeX

$$$a\cdot S = S.comap (MulSemiringAction.toRingAut(a)).symm$$$

Lean4

theorem pointwise_smul_eq_comap {a : M} (S : Ideal R) : a • S = S.comap (MulSemiringAction.toRingAut _ _ a).symm :=
  by
  ext
  simp [pointwise_smul_def]
  rfl

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