Theorem IsROrC.norm_I_of_ne_zero

Modification history

2024-03-28 10:26
Mathlib/Data/RCLike/Basic.lean
chore: Rename `IsROrC` to `RCLike` (#10819) …
Deleted IsROrC.norm_I_of_ne_zeroView on Github →
2023-07-14 11:17
Mathlib/Data/IsROrC/Basic.lean
chore: forward-port leanprover-community/mathlib#4798 (#5892)
Added IsROrC.norm_I_of_ne_zeroView on Github →