mathlib3
35ac2507
- Update src/data/complex/is_R_or_C.lean
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
Update src/data/complex/is_R_or_C.lean Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
References
#9692 - refactor(algebra/star): replace `star_ring_aut` with `star`
Author
dupuisf
Parents
233433b0
Loading