mathlib3
3c422528 - refactor(analysis/normed/group/hom): split (#18219)

Commit
2 years ago
refactor(analysis/normed/group/hom): split (#18219) Half of this file is completely elementary, able to be proved directly from the definitions in `normed/group/hom/basic` after a few instances are added there. The other half consists of technical lemmas from LTE, never used elsewhere in mathlib, and requires more imports. Since this file is imported by many files (including `data/complex/is_R_or_C`, see #18217 for a discussion of what that file imports), I propose splitting off the LTE half.
Author
Parents
Loading