Theorems · Theorem · category theory
Function.MulExact.apply_apply_eq_one
∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
Function.MulExact f g → ∀ (x : M), g (f x) = 1- Defined in
- Mathlib.Algebra.Exact.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- One
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.mem_range_selfproof · cited by 328
- Function.MulExactstatement and proof · cited by 28
Cited by5
Results whose statement or proof uses this declaration.
- MonoidHom.injective_of_surjective_of_injective_of_injectiveproof · cited by 2
- MonoidHom.surjective_of_surjective_of_surjective_of_injectiveproof · cited by 2
- Function.MulExact.comp_eq_oneproof · cited by 1
- MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injectiveproof · cited by 1
- TopologicalGroup.IsSES.inducedMeasure_lt_of_injOnproof · cited by 0