theorem star_ite {α : Type u_1} [has_involutive_star α] (P : Prop) [decidable P] (a b : α) :

theorem coe_ite {α : Type u_1} {β : Type u_2} [has_coe α β] (P : Prop) [decidable P] (a b : α) :

theorem ite_apply_lm {R : Type u_1} {A : Type u_2} {B : Type u_3} [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R A] [module R B] (f g : A →ₗ[R] B) (x : A) (P : Prop) [decidable P] :

theorem tensor_product.ite_map {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} [comm_semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄] [module R M₁] [module R M₂] [module R M₃] [module R M₄] (f₁ f₂ : M₁ →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (P : Prop) [decidable P] :