Theorems · Theorem · number theory
Northcott.comp_of_finite_fibers
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [inst : LE γ] [Northcott h']
[Filter.TendstoCofinite h], Northcott (h' ∘ h)A composition h' ∘ h is Northcott when h' is Northcott and the fibers of h are finite.
- Defined in
- Mathlib.Order.Northcott
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- Set.imageproof · cited by 5,609
- Set.Finite.subsetproof · cited by 285
- Filter.TendstoCofinitestatement and proof · cited by 28
- Northcottstatement and proof · cited by 19
- Filter.TendstoCofinite.finite_preimage_singletonproof · cited by 12
- Northcott.finite_leproof · cited by 8
- Set.Finite.inter_of_rightproof · cited by 4
- Set.Finite.of_finite_fibersproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.