Commit 2023-05-02 07:59 685bd4da

View on Github →

feat: port Data.Complex.Module (#3737)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Complex/Basic.lean

Created Mathlib/Data/Complex/Module.lean

added theorem AlgHom.map_coe_real_complex

added theorem Complex.algHom_ext

added theorem Complex.coe_algebraMap

added theorem Complex.coe_basisOneI

added theorem Complex.coe_basisOneI_repr

added theorem Complex.coe_smul

added def Complex.conjAe

added theorem Complex.conjAe_coe

added def Complex.equivRealProdAddHom

added def Complex.equivRealProdLm

added theorem Complex.finrank_real_complex

added theorem Complex.finrank_real_complex_fact

added def Complex.imLm

added theorem Complex.imLm_coe

added def Complex.lift

added def Complex.liftAux

added theorem Complex.liftAux_I

added theorem Complex.liftAux_apply

added theorem Complex.liftAux_apply_I

added theorem Complex.liftAux_neg_I

added def Complex.ofRealAm

added theorem Complex.ofRealAm_coe

added theorem Complex.rank_real_complex'.{u}

added theorem Complex.rank_real_complex

added def Complex.reLm

added theorem Complex.reLm_coe

added theorem Complex.real_algHom_eq_id_or_conj

added theorem Complex.real_smul

added theorem Complex.smul_im

added theorem Complex.smul_re

added theorem Complex.toMatrix_conjAe

added theorem finrank_real_of_complex

added theorem imaginaryPart_I_smul

added theorem imaginaryPart_apply_coe

added theorem imaginaryPart_smul

added theorem rank_real_of_complex

added theorem realPart_I_smul

added theorem realPart_add_I_smul_imaginaryPart

added theorem realPart_apply_coe

added theorem realPart_smul

added theorem skewAdjoint.I_smul_neg_I

added def skewAdjoint.negISMul