transitionMap_map_mul — Mathlib

English

The transition map is multiplicative: transitionMap(I,R,hmn)(x y) = transitionMap(I,R,hmn)(x) transitionMap(I,R,hmn)(y) in the quotient setting.

Русский

Переходная карта сохраняет умножение: переходная карта умножает значения функции.

LaTeX

$$$transitionMap(I,R,hmn)(x \cdot y) = transitionMap(I,R,hmn)(x) \cdot transitionMap(I,R,hmn)(y)$$$

Lean4

@[local simp]
theorem transitionMap_map_mul {m n : ℕ} (hmn : m ≤ n) (x y : R ⧸ (I ^ n • ⊤ : Ideal R)) :
    transitionMap I R hmn (x * y) = transitionMap I R hmn x * transitionMap I R hmn y :=
  Quotient.inductionOn₂' x y (fun _ _ ↦ rfl)

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