Theorems · Theorem · category theory
Function.MulExact.of_comp_of_mem_range
∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
g ∘ f = 1 → (∀ (x : N), g x = 1 → x ∈ Set.range f) → Function.MulExact f g- Defined in
- Mathlib.Algebra.Exact.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext, Quot.sound
- Assumes
- One
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.rangestatement and proof · cited by 4,705
- Function.MulExactstatement · cited by 28
Cited by1
Results whose statement or proof uses this declaration.
- MonoidHom.mulExact_of_comp_eq_one_of_ker_le_rangeproof · cited by 1