awayMap_mk — Mathlib

English

Applying awayMap to mk on Away yields the corresponding mk in the target away.

Русский

Применение awayMap к mk в Away даёт соответствующий mk в целевом Away.

LaTeX

$$$$ Away 𝒜 hg hx (mk \langle n, a, \langle f^i, hi \rangle, \langle i, rfl \rangle \rangle) = Away.mk 𝒜 (hx \Rightarrow mul_mem_graded hf hg) n (a \cdot g^i) (by rw [smul_add]; exact mul_mem_graded ha (pow_mem_graded n hg)). $$$$

Lean4

@[simp]
theorem awayMap_mk {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (a : A) (ha : a ∈ 𝒜 (n • d)) :
    awayMap 𝒜 hg hx (Away.mk 𝒜 hf n a ha) =
      Away.mk 𝒜 (hx ▸ mul_mem_graded hf hg) n (a * g ^ n)
        (by rw [smul_add]; exact mul_mem_graded ha (pow_mem_graded n hg)) :=
  by
  ext
  exact val_awayMap_mk ..

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