Theorems · Theorem · commutative algebra
Algebra.IsAlgebraic.isBaseChange_of_isFractionRing
∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (R' : Type u_4) (S' : Type u_5) [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [inst_6 : Algebra S S'] [IsFractionRing S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R S S'] [inst_10 : CommRing R'] [inst_11 : Algebra R R'] [IsFractionRing R R'] [inst_13 : Module R' S'] [inst_14 : IsScalarTower R R' S'], IsBaseChange R' (IsScalarTower.toAlgHom R S S').toLinearMap
- Defined in
- Mathlib.RingTheory.Algebraic.Integral
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- IsScalarTowerstatement and proof · cited by 3,896
- nonZeroDivisorsproof · cited by 895
- IsFractionRingstatement and proof · cited by 738
- NoZeroDivisorsstatement and proof · cited by 545
- FaithfulSMulstatement and proof · cited by 340
- Algebra.IsAlgebraicstatement and proof · cited by 322
- AlgHom.toLinearMapstatement and proof · cited by 254
- IsScalarTower.toAlgHomstatement and proof · cited by 232
- IsBaseChangestatement · cited by 87
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.