feat(field_theory/intermediate_field): Inhabited instance (#18956)

tb65536 · tb65536 · commit c596622fccd6 · 2023-05-08T17:26:30.000Z
If `S : intermediate_field K L`, then `S →ₐ[K] L` is nonempty.



Co-authored-by: Thomas Browning &lt;tb65536@users.noreply.github.com&gt;
diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
@@ -352,6 +352,8 @@ S.to_subalgebra.range_val
 @[simp] lemma field_range_val : S.val.field_range = S :=
 set_like.ext' subtype.range_val
 
+instance alg_hom.inhabited : inhabited (S →ₐ[K] L) := ⟨S.val⟩
+
 lemma aeval_coe {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
   [is_scalar_tower R K L] (x : S) (P : R[X]) : aeval (x : L) P = aeval x P :=
 begin
