TwoAdicDecomposition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two-adic form of a positive even square

Extract the power of two from an actual positive square root. Evenness of the square forces a positive exponent in that root, so squaring gives the precise form used at the start of the circulant Hadamard order reduction.

theorem OAI.CirculantHadamard.exists_two_adic_square_decomposition_of_eq_sq line 17

Source documentation

Extract the two-adic part from a specified positive square root.

theorem exists_two_adic_square_decomposition_of_eq_sq {n m : ℕ}
    (hm : 0 < m) (hnm : n = m ^ 2) (heven : Even n) :
    ∃ s u : ℕ, 1 ≤ s ∧ 0 < u ∧ Odd u ∧ n = 2 ^ (2 * s) * u ^ 2 := by
…

theorem OAI.CirculantHadamard.exists_two_adic_square_decomposition line 36

Source documentation

Every positive even natural square has a positive odd part and a nonzero, even power of two.

theorem exists_two_adic_square_decomposition {n : ℕ}
    (hn : 0 < n) (hsquare : IsSquare n) (heven : Even n) :
    ∃ s u : ℕ, 1 ≤ s ∧ 0 < u ∧ Odd u ∧ n = 2 ^ (2 * s) * u ^ 2 := by
…

theorem OAI.CirculantHadamard.exists_two_adic_square_decomposition_of_positive_square line 48

Source documentation

Interface for an order theorem that already supplies its positive root.

theorem exists_two_adic_square_decomposition_of_positive_square {n : ℕ}
    (hsquare : ∃ m : ℕ, 0 < m ∧ n = m ^ 2) (heven : Even n) :
    ∃ s u : ℕ, 1 ≤ s ∧ 0 < u ∧ Odd u ∧ n = 2 ^ (2 * s) * u ^ 2 := by
…