Source indexedlemma · leanprover/lean4:v4.32.0

RCLike.decomposition

Carleson.ToMathlib.Analysis.RCLike.Components · Carleson/ToMathlib/Analysis/RCLike/Components.lean:62 to 72

Mathematical statement

Exact Lean statement

lemma decomposition {𝕂 : Type*} [RCLike 𝕂] {a : 𝕂} :
  1 * ((algebraMap ℝ 𝕂) (component 1 a).toReal)
  + -1 * ((algebraMap ℝ 𝕂) (component (-1) a).toReal)
  + RCLike.I * ((algebraMap ℝ 𝕂) (component RCLike.I a).toReal)
  + -RCLike.I * ((algebraMap ℝ 𝕂) (component (-RCLike.I) a).toReal) = a

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma decomposition {𝕂 : Type*} [RCLike 𝕂] {a : 𝕂} :  1 * ((algebraMap ℝ 𝕂) (component 1 a).toReal)  + -1 * ((algebraMap ℝ 𝕂) (component (-1) a).toReal)  + RCLike.I * ((algebraMap ℝ 𝕂) (component RCLike.I a).toReal)  + -RCLike.I * ((algebraMap ℝ 𝕂) (component (-RCLike.I) a).toReal) = a := by  unfold component  simp only [map_one, mul_one, Real.coe_toNNReal', one_mul, map_neg, mul_neg, neg_mul,    RCLike.conj_I, RCLike.mul_re, RCLike.I_re, mul_zero, RCLike.I_im, zero_sub, neg_neg]  rw [← sub_eq_add_neg, ← sub_eq_add_neg, ← map_sub, add_sub_assoc, ← mul_sub, ← map_sub]  rw [max_zero_sub_eq_self, max_zero_sub_eq_self, mul_comm]  exact RCLike.re_add_im_ax a