R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin A s ≤ adjoin A ↑(adjoin R s)

R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ ↑(adjoin R s) ⊆ ↑(adjoin A s)
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin A ↑(adjoin R s) = adjoin A s
apply le_antisymm (adjoin_le _)
no goals
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin A s ≤ adjoin A ↑(adjoin R s)
exact adjoin_mono subset_adjoin
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin A s)
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ ↑(adjoin R s) ⊆ ↑(adjoin A s)
change adjoin R s ≤ (adjoin A s).restrictScalars R
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin A s)
refine' adjoin_le _
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
have : (Subalgebra.restrictScalars R (adjoin A s) : Set B) = adjoin A s := rfl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(adjoin A s)
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
rw [this]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(adjoin A s)
exact subset_adjoin