Module

QuadraticCompositum.lean

Nyll.SawinTotallyRealTowers.QuadraticCompositum

1 declaration indexed from sourceView source ↗

Module documentation

Square-class products inside intermediate fields

An intermediate field containing square roots of finitely many radicands also contains a square root of their product, up to a square in the base field. The proof constructs that root as an actual product and compares the two roots by their signs.

Imports3

Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.Ring.Commute

Imported by2

theorem

squareRoot_mem_of_squareClass_product

L28 ↗

ClassFieldTower.Sawin.squareRoot_mem_of_squareClass_product

Documentation

A finite product of known square roots realizes a product of square classes inside the same intermediate field.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v w
namespace ClassFieldTower.Sawin
open scoped BigOperators

Lean source · statement

theorem squareRoot_mem_of_squareClass_product
    {F : Type u} {E : Type v} {ι : Type w}
    [Field F] [Field E] [Algebra F E]
    (K : IntermediateField F E) (s : Finset ι)
    (d : ι → F) (β : ι → E) (a q : F) (α : E)
    (hα : α ^ 2 = algebraMap F E a)
    (hβ : ∀ i ∈ s, β i ^ 2 = algebraMap F E (d i))
    (hMem : ∀ i ∈ s, β i ∈ K)
    (hClass : a = (∏ i ∈ s, d i) * q ^ 2) : α ∈ K

Module documentation

Square-class products inside intermediate fields

Declarations

squareRoot_mem_of_squareClass_product