Theorems · Definition · commutative algebra

Algebra.QuasiFinite.casesOn

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {motive : Algebra.QuasiFinite R S → Sort u} →
            (t : Algebra.QuasiFinite R S) →
              ((finite_fiber : ∀ (P : Ideal R) [inst_3 : P.IsPrime], Module.Finite P.ResidueField (P.Fiber S)) →
                  motive ⋯) →
                motive t

Defined in

Mathlib.RingTheory.QuasiFinite.Basic

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra