algebraicIndependent_empty — Mathlib

English

If the index type is empty and A is nontrivial, then the trivial family is algebraically independent over K.

Русский

Если индексный тип пуст, а A нетривиален, то тривиальная совокупность независима над K.

LaTeX

$$$\text{algebraicIndependent_empty_type}$$$

Lean4

theorem algebraicIndependent_empty [Nontrivial A] : AlgebraicIndependent K ((↑) : (∅ : Set A) → A) :=
  algebraicIndependent_empty_type

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