isAlgebraic_iff — Mathlib

English

A subalgebra is algebraic iff its underlying algebra is algebraic.

Русский

Подалгебра алгебраическая тогда и только тогда, когда она алгебраическая как алгебра.

LaTeX

$$$S.IsAlgebraic \\iff Algebra.IsAlgebraic R S$$$

Lean4

/-- A subalgebra is algebraic if and only if it is algebraic as an algebra. -/
theorem isAlgebraic_iff (S : Subalgebra R A) : S.IsAlgebraic ↔ Algebra.IsAlgebraic R S :=
  by
  delta Subalgebra.IsAlgebraic
  rw [Subtype.forall', Algebra.isAlgebraic_def]
  refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_
  have h : Function.Injective S.val := Subtype.val_injective
  conv_rhs => rw [← h.eq_iff, map_zero]
  rw [← aeval_algHom_apply, S.val_apply]

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