Mathlib Map

Theorems · Inductive type

CompTriple

{M : Type u_1} → {N : Type u_2} → {P : Type u_3} → (M → N) → (N → P) → outParam (M → P) → Prop

Class of composing triples

Defined in
Mathlib.Logic.Function.CompTypeclasses
Cited by
11 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CompTriple.comp_eq · cited by 51CompTriple.comp_eqMulActionHom.comp · cited by 12MulActionHom.compAddActionHom.comp · cited by 10AddActionHom.compCompTriple.comp_inv · cited by 4CompTriple.comp_invAddActionHom.comp_apply · cited by 2AddActionHom.comp_applyMulActionHom.comp_apply · cited by 2MulActionHom.comp_applyMulAction.stabilizerEquivStabilizer_compTriple · cited by 1MulAction.stabilizerEquiv…AddAction.stabilizerEquivStabilizer_compTriple · cited by 1AddAction.stabilizerEquiv…AddActionHom.comp_assoc · cited by 0AddActionHom.comp_assocCompTriple.casesOn · cited by 0CompTriple.casesOnCompTriple.comp · cited by 0CompTriple.compCompTriple.comp_apply · cited by 0CompTriple.comp_applyCompTriple.recOn · cited by 0CompTriple.recOnMulActionHom.comp.congr_simp · cited by 0comp.congr_simpMulActionHom.comp_assoc · cited by 0MulActionHom.comp_assocCompTripleCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by15

Results whose statement or proof uses this declaration.