square root of 1

Stream: Is there code for X?

[Michael Stoll]

Is this is mathlib?

lemma sqrt_of_one (R : Type*) [comm_ring R] [no_zero_divisors R] (a : R) (ha : a^2 = 1) : a = 1 ∨ a = -1 := sorry

There is docs#sq_eq_one_iff, but this requires linear_ordered_ring R, which I don't have in my use case (where R is a finite field). Grepping mathlib for either .* ^2 = 1 or \(.*\) = 1 ∨ \1 = -1 doesn't come up with anything else that gets remotely close.

[Damiano Testa]

Not really an answer, but don't division ring and comm ring introduce two ring structures?

[Damiano Testa]

Did you mean to use field? Or did you want something more general?

[Yaël Dillies]

Isn't a commutative division ring simply a field?

[Michael Stoll]

Sorry, I got confused. I meant [comm_ring R] [no_zero_divisors R](i.e., R is a domain). It is getting late...

[Michael Stoll]

I'll edit the code above.

[Eric Wieser]

Ah yes, docs#linear_ordered_ring.is_domain