feat(RingTheory): no extension is algebraic over the zero ring (leanprover-community#33540)

Author: YaelDillies

Mathlib/RingTheory/Algebraic/Defs.lean

@@ -62,18 +62,21 @@ theorem transcendental_iff {x : A} :
 protected def Subalgebra.IsAlgebraic (S : Subalgebra R A) : Prop :=
   ∀ x ∈ S, IsAlgebraic R x
 
-variable (R A)
-
+variable (R A) in
 /-- An algebra is algebraic if all its elements are algebraic. -/
 @[stacks 09GC "Algebraic extensions"]
 protected class Algebra.IsAlgebraic : Prop where
   isAlgebraic : ∀ x : A, IsAlgebraic R x
 
+variable (R A) in
 /-- An algebra is transcendental if some element is transcendental. -/
 protected class Algebra.Transcendental : Prop where
   transcendental : ∃ x : A, Transcendental R x
 
-variable {R A}
+variable (R A) in
+lemma Algebra.nontrivial_of_isAlgebraic [Algebra.IsAlgebraic R A] : Nontrivial R := by
+  obtain ⟨p, hp, -⟩ := Algebra.IsAlgebraic.isAlgebraic (R := R) (0 : A)
+  exact .of_polynomial_ne hp
 
 lemma Algebra.isAlgebraic_def : Algebra.IsAlgebraic R A ↔ ∀ x : A, IsAlgebraic R x :=
   ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩