Theorems · Theorem · group theory
smul_ite
∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a b : α) (c : β),
(c • if p then a else b) = if p then c • a else c • b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 26 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.
- smul_diteproof · cited by 2
Cited by26
Results whose statement or proof uses this declaration.
- Matrix.smul_singleproof · cited by 5
- Matrix.toLinearMap₂'Aux_singleproof · cited by 5
- LieAlgebra.Basis.baseSupp_apply_h'proof · cited by 3
- ProbabilityTheory.setBernoulli_singletonproof · cited by 3
- RootPairing.GeckConstruction.lie_h_eproof · cited by 2
- Matrix.mulVecLin_oneproof · cited by 2
- LinearMap.IsSymmetric.toMatrix_eigenvectorBasisproof · cited by 2
- HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_posproof · cited by 2
- Finset.indicator_biUnion_eq_sum_powersetproof · cited by 1
- QuadraticMap.toQuadraticMap_toBilinproof · cited by 1
- HahnSeries.SummableFamily.support_powerSeriesFamily_subsetproof · cited by 1
- GeneralSchauderBasis.proj_compproof · cited by 1