Theorems · Theorem
add_ite
∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a b c : α),
(a + if P then b else c) = if P then a + b else a + c- Defined in
- Mathlib.Algebra.Notation.Defs
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_diteproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- Pi.single_add_single_eq_single_add_singleproof · cited by 1
- dist_indicatorproof · cited by 1
- Nat.card_multiplesproof · cited by 0
- Nat.Ioc_filter_dvd_card_eq_divproof · cited by 0