Some stuff on dites

theorem hMul_dite {α : Type u_1} [Mul α] (P : Prop) [Decidable P] (a : α) (b : P → α) (c : ¬P → α) : (a * if x : P then b x else c x) = if x : P then a * b x else a * c x

theorem dite_hMul {α : Type u_1} [Mul α] (P : Prop) [Decidable P] (a : α) (b : P → α) (c : ¬P → α) : (if x : P then b x else c x) * a = if x : P then b x * a else c x * a

theorem dite_boole_add {α : Type u_1} [AddZeroClass α] (P : Prop) [Decidable P] (a : P → α) (b : P → α) : (if x : P then a x + b x else 0) = (if x : P then a x else 0) + if x : P then b x else 0

theorem dite_boole_smul {α : Type u_1} {β : Type u_2} [Zero α] [SMulZeroClass β α] (P : Prop) [Decidable P] (a : P → α) (r : β) : (if x : P then r • a x else 0) = r • if x : P then a x else 0

theorem star_dite (P : Prop) [Decidable P] {α : Type u_1} [InvolutiveStar α] (a : P → α) (b : ¬P → α) : star (if i : P then a i else b i) = if i : P then star (a i) else star (b i)

theorem dite_tmul {R : Type u_1} {N₁ : Type u_2} {N₂ : Type u_3} [CommSemiring R] [AddCommGroup N₁] [AddCommGroup N₂] [Module R N₁] [Module R N₂] (P : Prop) [Decidable P] (x₁ : P → N₁) (x₂ : N₂) : (if h : P then x₁ h else 0) ⊗ₜ[R] x₂ = if h : P then x₁ h ⊗ₜ[R] x₂ else 0

theorem tmul_dite {R : Type u_1} {N₁ : Type u_2} {N₂ : Type u_3} [CommSemiring R] [AddCommGroup N₁] [AddCommGroup N₂] [Module R N₁] [Module R N₂] (P : Prop) [Decidable P] (x₁ : N₁) (x₂ : P → N₂) : (x₁ ⊗ₜ[R] if h : P then x₂ h else 0) = if h : P then x₁ ⊗ₜ[R] x₂ h else 0

theorem LinearMap.apply_dite {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [Semiring R] [AddCommMonoid H₁] [AddCommMonoid H₂] [Module R H₁] [Module R H₂] (f : H₁ →ₗ[R] H₂) (P : Prop) [Decidable P] (a : P → H₁) (b : ¬P → H₁) : f (if h : P then a h else b h) = if h : P then f (a h) else f (b h)

theorem dite_apply' {i : Type u_1} {β : Type u_2} {α : i → Type u_3} (P : Prop) [Decidable P] {j : i} (f : P → β → α j) [Zero (α j)] (a : β) : (if h : P then f h else 0) a = if h : P then f h a else 0