instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul

English

There exists a nonempty subset s of A such that AlgebraicIndepOn R id s, provided the action of R on A is faithful.

Русский

Существет не пустое подмножество s ⊆ A такое, что AlgebraicIndepOn R id s при условии, что действие R на A верно faithfully.

LaTeX

$$$\\\\exists s:\\\\Set A, s \\\\text{ nonempty} \\\\land \\\\text{AlgebraicIndepOn}(R, id, s)$$$

Lean4

instance [FaithfulSMul R A] : Nonempty { s : Set A // AlgebraicIndepOn R id s } :=
  ⟨∅, algebraicIndependent_empty_type_iff.mpr <| FaithfulSMul.algebraMap_injective R A⟩

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