Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit ae69578

Browse files
committed
fix(ring_theory/algebraic): Make is_transcendental_of_subsingleton fully general (#12870)
I mistyped a single letter.
1 parent 706a824 commit ae69578

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/ring_theory/algebraic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ def is_algebraic (x : A) : Prop :=
3232
/-- An element of an R-algebra is transcendental over R if it is not algebraic over R. -/
3333
def transcendental (x : A) : Prop := ¬ is_algebraic R x
3434

35-
lemma is_transcendental_of_subsingleton [subsingleton R] (x : R) : transcendental R x :=
35+
lemma is_transcendental_of_subsingleton [subsingleton R] (x : A) : transcendental R x :=
3636
λ ⟨p, h, _⟩, h $ subsingleton.elim p 0
3737

3838
variables {R}

0 commit comments

Comments
 (0)