theorem
L21 ↗symbol_mul_right
ClassFieldTheory.HilbertPairing.symbol_mul_right
The symbol is multiplicative in its second representative.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory.HilbertPairing
universe uLean source · statement
theorem symbol_mul_right
{K : Type u} [Field K] {n : ℕ+}
(B : HilbertPairing K n) (a b c : Kˣ) :
B.symbol a (b * c) = B.symbol a b * B.symbol a c