mathlib
9b946bf9 - use one := 1 advice for field.to_euclidean_domain
Commit
View On GitHub
Commit
5 years ago
use one := 1 advice for field.to_euclidean_domain
Author
ChrisHughes24 ChrisHughes24
Parents
9e7ed943
FAQ Terms Privacy Refunds Impressum
Loading