Theorems · Theorem · field theory
IntermediateField.adjoin_adjoin_left
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) =
IntermediateField.adjoin F (S ∪ T)Adjoining S and then T is the same as adjoining S ∪ T.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- Algebra.algebraMapproof · cited by 4,706
- Set.rangeproof · cited by 4,705
- IntermediateFieldstatement · cited by 988
- IntermediateField.adjoinstatement and proof · cited by 382
- subset_antisymmproof · cited by 150
- Set.subset_union_leftproof · cited by 142
- Set.subset_union_rightproof · cited by 123
- Set.range_subset_iffproof · cited by 99
Cited by6
Results whose statement or proof uses this declaration.
- IntermediateField.restrictScalars_adjoinproof · cited by 9
- IntermediateField.adjoin_simple_adjoin_simpleproof · cited by 3
- IntermediateField.adjoin_adjoin_commproof · cited by 2
- Polynomial.irreducible_compproof · cited by 1
- IntermediateField.induction_on_adjoin_finsetproof · cited by 1
- Field.Emb.Cardinal.filtration_succproof · cited by 0