Commit 2025-05-19 08:29 82c80d8c
View on Github →feat(NumberField): define the maximalRealSubfield of a number field (#23760)
Define the maximalRealSubfield of a number field. It is a totally real subfield that contains all other totally real subfields.
Add also a couple of instances about the fact that subfields of a totally real field are totally real.