Mathlib Changelog
v4
Changelog
About
Github
Theorem
Complex.integerComplement.ne_zero
Modification history
2024-11-15 10:19
Mathlib/Analysis/Complex/IntegerCompl.lean
feat(Analysis): integer complement in `ℂ` (#16542) …
Added
Complex.integerComplement.ne_zero
View on Github →