Norm

Stream: new members

[亚历山大大帝]

Does there exist a theorem in Mathlib that characterizes the structure of elements with norm 1 in field extensions? The core idea can be summarized as follows: In a cyclic extension, an element with norm 1 must be the quotient of an element and its image under the action of the Galois group?