Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-19 22:26 56115334

View on Github →

feat(analysis/normed_space/star/complex): real and imaginary part of an element of a star module (#11811) We introduce the real and imaginary parts of an element of a star module, and show that elements of the type can be decomposed into these two parts in the obvious way.

Estimated changes

Modified src/algebra/invertible.lean

added theorem inv_of_two_add_inv_of_two

Modified src/algebra/module/basic.lean

added theorem inv_of_two_smul_add_inv_of_two_smul

Modified src/algebra/star/module.lean

added def self_adjoint.submodule

added def self_adjoint_part

added def skew_adjoint.submodule

added def skew_adjoint_part

added def star_module.decompose_prod_adjoint

added theorem star_module.self_adjoint_part_add_skew_adjoint_part

Modified src/analysis/normed_space/exponential.lean

Created src/analysis/normed_space/star/complex.lean

added def star_module.mul_neg_I_lin

added theorem star_module.re_add_im

Modified src/analysis/special_functions/exponential.lean

Modified src/data/complex/basic.lean

added theorem complex.conj_inv

modified theorem complex.star_def

Modified src/data/complex/is_R_or_C.lean

deleted theorem is_R_or_C.char_zero_R_or_C

added theorem is_R_or_C.conj_inv

added theorem is_R_or_C.star_def

Modified src/data/complex/module.lean