theorem
L22 ↗symbol_mul_left
ClassFieldTheory.HilbertPairing.symbol_mul_left
The symbol is multiplicative in its first 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_left
{K : Type u} [Field K] {n : ℕ+}
(B : HilbertPairing K n) (a b c : Kˣ) :
B.symbol (a * b) c = B.symbol a c * B.symbol b c