mathlib3
ec2f3509 - feat(field_theory/intermediate_field): Range of `intermediate_field.val` (#10873)

Commit

4 years ago

feat(field_theory/intermediate_field): Range of `intermediate_field.val` (#10873) The range of the algebra homomorphism `S.val` equals `S.to_subalgebra`.

Author

tb65536

Parents

718ea932

mathlib3 ec2f3509 - feat(field_theory/intermediate_field): Range of `intermediate_field.val` (#10873)

mathlib3
ec2f3509 - feat(field_theory/intermediate_field): Range of `intermediate_field.val` (#10873)