Theorems · Definition · commutative algebra

Algebra.FiniteType.casesOn

{R : Type uR} →
  {A : Type uA} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {motive : Algebra.FiniteType R A → Sort u} →
            (t : Algebra.FiniteType R A) → ((out : ⊤.FG) → motive ⋯) → motive t

Defined in: Mathlib.RingTheory.FiniteType
Cited by: 5 results in Mathlib
Foundations: Depth 77 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.

Cites7

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

Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Top.topstatement and proof · cited by 9,680
Subalgebrastatement · cited by 1,353
Algebra.FiniteTypestatement and proof · cited by 84
Subalgebra.FGstatement and proof · cited by 45

Cited by5

Results whose statement or proof uses this declaration.

AlgebraicGeometry.exists_lift_of_germInjective_auxproof · cited by 1
Algebra.FiniteType.iff_quotient_freeAlgebraproof · cited by 1
Algebra.FiniteType.iff_quotient_mvPolynomialproof · cited by 1
AddMonoidAlgebra.exists_finset_adjoin_eq_topproof · cited by 1
MonoidAlgebra.exists_finset_adjoin_eq_topproof · cited by 0