weierstrassDistinguished_smul — Mathlib

English

If a is a scalar and ga is a Weierstrass factorization of a g, then the distinguished part of a g is a times the distinguished part of g.

Русский

Если скаляр a умножает g, то отличительная часть a g равна a умноженному на отличительную часть g.

LaTeX

$$$(a \cdot g)^{\text{dist}} = a \cdot g^{\text{dist}}$$$

Lean4

@[simp]
theorem weierstrassDistinguished_smul (hg : (a • g).map (IsLocalRing.residue A) ≠ 0) :
    (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished (fun h ↦ hg (by simp [Algebra.smul_def, h])) :=
  by
  have H :=
    g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit (fun h ↦ hg (by simp [Algebra.smul_def, h]))
  have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
  have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
  exact (H'.elim (H.smul (by simpa using ha))).1

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