Def NumberField.mixedEmbedding.normAtPlace

Modification history