Commit 2021-12-24 13:57 7c7195f6

feat(field_theory/adjoin): lemmas about infs of intermediate_fields (#10997) This adjusts the data in the galois_insertion slightly such that this new lemma is true by rfl, to match how we handle this in subalgebra. As a result, top_to_subalgebra is now refl, but adjoin_univ is no longer refl. This also adds a handful of trivial simp lemmas.