sumElim_iff — Mathlib

English

A reformulation of the previous result with complement of a subset.

Русский

Переформулировка предыдущего результата с дополнением подмножества.

LaTeX

$$$\forall {x} {s},\ AlgebraicIndependent R x \iff AlgebraicIndependent R (fun i => x i) ∧ AlgebraicIndepOn (adjoin R (x '' sᶜ)) x s$$

Lean4

theorem sumElim_iff {ι'} {y : ι' → A} :
    AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (adjoin R (range x)) y :=
  by
  by_cases hx : AlgebraicIndependent R x; swap
  · exact ⟨fun h ↦ (hx <| by apply h.comp _ Sum.inr_injective).elim, fun h ↦ (hx h.1).elim⟩
  let e := (sumAlgEquiv R ι' ι).trans (mapAlgEquiv _ hx.aevalEquiv)
  have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by ext (_ | _) <;> simp [e]
  simp_rw [hx, AlgebraicIndependent, this]; simp

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