weierstrassUnit_smul — Mathlib

English

If a is a scalar and ga is a Weierstrass factorization, then the unit part scales by a.

Русский

Если скаляр умножает g, то единичная часть факторизации масштабируется на тот же скаляр.

LaTeX

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

Lean4

@[simp]
theorem weierstrassUnit_smul (hg : (a • g).map (IsLocalRing.residue A) ≠ 0) :
    (a • g).weierstrassUnit hg = a • g.weierstrassUnit (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))).2

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