The meta properties of quasi-finite ring homomorphisms.

def RingHom.QuasiFinite {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A ring hom R →+* S is quasi-finite if S is a quasi-finite R-algebra.

theorem RingHom.QuasiFinite.toAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.QuasiFinite) : Algebra.QuasiFinite R S

Helper lemma for the algebraize tactic

theorem RingHom.quasiFinite_algebraMap {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).QuasiFinite ↔ Algebra.QuasiFinite R S

theorem RingHom.QuasiFinite.comp {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (hf : f.QuasiFinite) (hg : g.QuasiFinite) : (f.comp g).QuasiFinite

theorem RingHom.QuasiFinite.of_comp {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (h : (f.comp g).QuasiFinite) : f.QuasiFinite

theorem RingHom.QuasiFinite.comp_iff {T : Type u_3} [CommRing T] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : S →+* T} {g : R →+* S} (hg : g.QuasiFinite) : (f.comp g).QuasiFinite ↔ f.QuasiFinite

theorem RingHom.QuasiFinite.of_finite {T : Type u_3} [CommRing T] {S : Type u_5} [CommRing S] {f : S →+* T} (hf : f.Finite) : f.QuasiFinite

theorem RingHom.QuasiFinite.stableUnderComposition : StableUnderComposition fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.respectsIso : RespectsIso fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.isStableUnderBaseChange : IsStableUnderBaseChange fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.holdsForLocalizationAway : HoldsForLocalizationAway fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.ofLocalizationSpanTarget : OfLocalizationSpanTarget fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.propertyIsLocal : PropertyIsLocal fun {R S : Type u_6} [CommRing R] [CommRing S] => QuasiFinite

theorem RingHom.QuasiFinite.of_isIntegral_of_finiteType {R : Type u_6} {S : Type u_7} {T : Type u_8} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} (hf : f.IsIntegral) {g : S →+* T} (hg : g.IsStandardOpenImmersion) : (g.comp f).FiniteType → (g.comp f).QuasiFinite

If T is both a finite type R-algebra, and the localization of an integral R-algebra, then T is quasi-finite over R

@[reducible, inline]

abbrev RingHom.QuasiFiniteAt {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] (f : R →+* S) (p : Ideal S) [p.IsPrime] : Prop

The predicate for a ring hom being quasi-finite at a prime.