mathlib3
52495a0f
- chore(data/set/lattice): fix name (#9520)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(data/set/lattice): fix name (#9520) `comp` is for composition, `compl` for complement. Fix names using `comp` instead of `compl`.
Author
sgouezel
Parents
465508fc
Loading