Theorems · Theorem · commutative algebra

Algebra.FiniteType.of_restrictScalars_finiteType

∀ (R : Type uR) (S : Type uS) (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [hA : Algebra.FiniteType R A], Algebra.FiniteType S A

Defined in: Mathlib.RingTheory.FiniteType
Cited by: 3 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring Semiring Algebra Algebra Algebra IsScalarTower Algebra.FiniteType

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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
Finsetproof · cited by 13,712
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Top.topproof · cited by 9,680
SetLike.coeproof · cited by 8,199
IsScalarTowerstatement and proof · cited by 3,896
Algebra.adjoinproof · cited by 535
Algebra.subset_adjoinproof · cited by 109
Algebra.FiniteTypestatement and proof · cited by 84
Subalgebra.restrictScalarsproof · cited by 36
Algebra.adjoin_leproof · cited by 36

Cited by3

Results whose statement or proof uses this declaration.

RingHom.FiniteType.of_comp_finiteTypeproof · cited by 3
Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐproof · cited by 1
Algebra.QuasiFinite.of_isIntegral_of_finiteTypeproof · cited by 1