Commit 2023-05-20 13:50 63bcb96b

View on Github →

feat: port Data.IsROrC.Lemmas (#4141)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/IsROrC/Lemmas.lean

added theorem FiniteDimensional.proper_isROrC

added theorem IsROrC.conjCle_norm

added theorem IsROrC.ofRealClm_norm

added theorem IsROrC.reClm_norm

added theorem Polynomial.ofReal_eval