Commit 2023-02-28 08:27 a8d52095

View on Github →

feat: Port Data.Real.ConjugateExponents (#2411) Rename and reflow only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/ConjugateExponents.lean

added theorem Real.IsConjugateExponent.conj_eq

added theorem Real.IsConjugateExponent.conjugate_eq

added theorem Real.IsConjugateExponent.div_conj_eq_sub_one

added theorem Real.IsConjugateExponent.inv_add_inv_conj_ennreal

added theorem Real.IsConjugateExponent.inv_add_inv_conj_nNReal

added theorem Real.IsConjugateExponent.mul_eq_add

added theorem Real.IsConjugateExponent.ne_zero

added theorem Real.IsConjugateExponent.nonneg

added theorem Real.IsConjugateExponent.one_div_ne_zero

added theorem Real.IsConjugateExponent.one_div_nonneg

added theorem Real.IsConjugateExponent.one_div_pos

added theorem Real.IsConjugateExponent.one_lt_nNReal

added theorem Real.IsConjugateExponent.pos

added theorem Real.IsConjugateExponent.sub_one_mul_conj

added theorem Real.IsConjugateExponent.sub_one_ne_zero

added theorem Real.IsConjugateExponent.sub_one_pos

added structure Real.IsConjugateExponent

added def Real.conjugateExponent

added theorem Real.isConjugateExponent_conjugateExponent

added theorem Real.isConjugateExponent_iff

added theorem Real.isConjugateExponent_one_div