mathlib
ff548cdd - feat(field_theory/adjoin): `F⟮α⟯ ≤ K ↔ α ∈ K` (#15420)

Commit

3 years ago

feat(field_theory/adjoin): `F⟮α⟯ ≤ K ↔ α ∈ K` (#15420) I was surprised that we didn't have this lemma already.

References

Author

tb65536

Parents