Commit 2024-10-01 21:09 ac1e7e83

View on Github →

feat: Composition of the coercion ℝ → ℂ with algebraic operations (#17213) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Group/Hom/Defs.lean

modified theorem map_comp_pow

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.ofReal_comp_add

added theorem Complex.ofReal_comp_mul

added theorem Complex.ofReal_comp_neg

added theorem Complex.ofReal_comp_nsmul

added theorem Complex.ofReal_comp_pow

added theorem Complex.ofReal_comp_sub

added theorem Complex.ofReal_comp_zsmul