Theorems · Theorem · commutative algebra

Algebra.adjoin_res_eq_adjoin_res

∀ (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : Type u_4) [inst : CommSemiring C] [inst_1 : CommSemiring D]
  [inst_2 : CommSemiring E] [inst_3 : CommSemiring F] [inst_4 : Algebra C D] [inst_5 : Algebra C E]
  [inst_6 : Algebra C F] [inst_7 : Algebra D F] [inst_8 : Algebra E F] [inst_9 : IsScalarTower C D F]
  [inst_10 : IsScalarTower C E F] {S : Set D} {T : Set E},
  Algebra.adjoin C S = ⊤ →
    Algebra.adjoin C T = ⊤ →
      Subalgebra.restrictScalars C (Algebra.adjoin E (⇑(algebraMap D F) '' S)) =
        Subalgebra.restrictScalars C (Algebra.adjoin D (⇑(algebraMap E F) '' T))

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites21

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
Setstatement and proof · cited by 53,352
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
RingHomstatement and proof · cited by 10,189
Top.topstatement and proof · cited by 9,680
Set.imagestatement and proof · cited by 5,609
Algebra.algebraMapstatement and proof · cited by 4,706
IsScalarTowerstatement and proof · cited by 3,896
Subalgebrastatement and proof · cited by 1,353
RingHomClass.toRingHomproof · cited by 746
Algebra.adjoinstatement and proof · cited by 535

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.