Theorems · Theorem · general algebraic systems
mul_apply_eq_comp
∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : Mul F} [self : IsMulApplyEqComp F α]
(f g : F) (x : α), (f * g) x = f (g x)Alias of IsMulApplyEqComp.mul_apply_eq_comp.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- IsMulApplyEqComp
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- FunLikestatement · cited by 2,560
- IsMulApplyEqCompstatement · cited by 7
- IsMulApplyEqComp.mul_apply_eq_compproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.isTopCompl_range_ker_of_leftInverseproof · cited by 3
- ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquivproof · cited by 2
- ContinuousLinearMap.isStarNormal_iff_norm_eq_adjointproof · cited by 2
- ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormalproof · cited by 2
- FunLike.coe_mul_eq_compproof · cited by 1
- pow_apply_eq_iterateproof · cited by 1
- RKHS.posSemidef_kernelproof · cited by 0
- HasDerivAt.norm_sqproof · cited by 0
- HasDerivWithinAt.norm_sqproof · cited by 0
- ContinuousLinearMap.mul_applyproof · cited by 0