of_mul_unit — Mathlib

English

If R,A,S,SA are configured in a pushout square with integral R-S data, then Algebra.IsIntegral A SA holds.

Русский

При конфигурации в квадрате-пуше (pushout) с данными интегрированности по R для R,S, A, SA выполняется условие Algebra.IsIntegral A SA.

LaTeX

$$$Algebra.IsIntegral A SA$$$

Lean4

theorem of_mul_unit {x y : B} {r : R} (hr : algebraMap R B r * y = 1) (hx : IsIntegral R (x * y)) : IsIntegral R x :=
  by
  obtain ⟨p, p_monic, hp⟩ := hx
  refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩
  convert scaleRoots_aeval_eq_zero hp
  rw [Algebra.commutes] at hr ⊢
  rw [mul_assoc, hr, mul_one]; rfl

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