Theorems · Inductive type · general algebraic systems
IsDivApply
(F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Div β] → [Div F] → Prop
IsDivApply F α β states for all f g : F and x : α, (f / g) x = f x / g x.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 3 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.
- FunLikestatement · cited by 2,560
Cited by11
Results whose statement or proof uses this declaration.
- div_applystatement · cited by 1
- IsDivApply.div_applystatement and proof · cited by 1
- IsDivApply.casesOnstatement and proof · cited by 0
- IsDivApply.recOnstatement and proof · cited by 0
- FunLike.coe_divstatement and proof · cited by 0
- FunLike.commGroupstatement and proof · cited by 0
- FunLike.divInvMonoidstatement and proof · cited by 0
- FunLike.divInvOneMonoidstatement and proof · cited by 0
- FunLike.divisionCommMonoidstatement and proof · cited by 0
- FunLike.divisionMonoidstatement and proof · cited by 0
- FunLike.groupstatement and proof · cited by 0