subalgebraNontrivial — Mathlib

English

If A is a nontrivial ring, then the subalgebra of polynomials over A is nontrivial.

Русский

Если A не тривиально как кольцо, то подалгебра полиномов над A не тривиальна.

LaTeX

$$$\mathrm{Nontrivial}\; (\mathrm{Subalgebra}\; R\; (A[X]))$$$

Lean4

instance subalgebraNontrivial [Nontrivial A] : Nontrivial (Subalgebra R A[X]) :=
  ⟨⟨⊥, ⊤, by
      rw [Ne, SetLike.ext_iff, not_forall]
      refine ⟨X, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top, algebraMap_apply]
      intro x
      rw [ext_iff, not_forall]
      refine ⟨1, ?_⟩
      simp⟩⟩

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