Theorems · Definition · commutative algebra

Algebra.FinitePresentation.casesOn

{R : Type w₁} →
  {A : Type w₂} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {motive : Algebra.FinitePresentation R A → Sort u} →
            (t : Algebra.FinitePresentation R A) →
              ((out : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → motive ⋯) → motive t

Defined in: Mathlib.RingTheory.FinitePresentation
Cited by: 4 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring Semiring Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
RingHomstatement · cited by 10,189
Finsuppstatement · cited by 5,255
AlgHomstatement and proof · cited by 3,236
MvPolynomialstatement and proof · cited by 2,140
AlgHom.toRingHomstatement and proof · cited by 490
RingHom.kerstatement and proof · cited by 363
Ideal.FGstatement and proof · cited by 99
Algebra.FinitePresentationstatement and proof · cited by 56

Cited by4

Results whose statement or proof uses this declaration.

RingHom.FinitePresentation.polynomial_inductionproof · cited by 1
Algebra.FinitePresentation.iffproof · cited by 1
Algebra.FinitePresentation.iff_quotient_mvPolynomial'proof · cited by 1
RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimitproof · cited by 1