NYLL
Module

ProductArgument.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalCoreBase.ProductArgument
25 declarations indexed from sourceView source ↗

Module documentation

The two-variable formal logarithm product argument

This module defines X + Y + XY, its logarithmic substitution, and the support description needed for the formal product formula.

Imports3
Imported by3

Declarations

def

formalLogOnePlusProductArgument

L29 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument
Documentation

The two-variable argument of the product formula: (1 + X) * (1 + Y) - 1 = X + Y + X*Y.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
def formalLogOnePlusProductArgument
    (A : Type*) [CommRing A] : MvPowerSeries (Fin 2) A
def

formalLogOnePlusProductArgumentPolynomial

L36 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentPolynomial
Documentation

The polynomial incarnation of the two-variable product argument (1 + X) * (1 + Y) - 1 = X + Y + XY.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
def formalLogOnePlusProductArgumentPolynomial
    (A : Type*) [CommSemiring A] : MvPolynomial (Fin 2) A
theorem

formalLogOnePlusProductArgument_eq_coe_polynomial

L43 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_eq_coe_polynomial
Documentation

The formal product argument is the power-series image of the corresponding finite polynomial.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_eq_coe_polynomial
    (A : Type*) [CommRing A] :
    formalLogOnePlusProductArgument A =
      (formalLogOnePlusProductArgumentPolynomial A :
        MvPowerSeries (Fin 2) A)
theorem

formalLogOnePlusProductArgumentPolynomial_eval_pair

L53 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgumentPolynomial_eval_pair
Documentation

Evaluating the polynomial product argument at (x,y) gives x + y + xy.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgumentPolynomial_eval_pair
    (A : Type*) [CommSemiring A] (x y : A) :
    MvPolynomial.eval (fun i : Fin 2 => if i = 0 then x else y)
        (formalLogOnePlusProductArgumentPolynomial A) =
      x + y + x * y := by
  simp [formalLogOnePlusProductArgumentPolynomial]
theorem

formalLogOnePlusProductArgument_eq_mul_sub_one

L64 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_eq_mul_sub_one
Documentation

Establishes the identity formalLogOnePlusProductArgument A = (1 + MvPowerSeries.X (0 : Fin 2)) * (1 + MvPowerSeries.X (1 : Fin 2)) - 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_eq_mul_sub_one
    (A : Type*) [CommRing A] :
    formalLogOnePlusProductArgument A =
      (1 + MvPowerSeries.X (0 : Fin 2)) *
          (1 + MvPowerSeries.X (1 : Fin 2)) - 1
theorem

formalLogOnePlusProductArgument_one_add

L76 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_one_add
Documentation

Adding one to the product argument recovers (1 + X) * (1 + Y).

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_one_add
    (A : Type*) [CommRing A] :
    1 + formalLogOnePlusProductArgument A =
      (1 + MvPowerSeries.X (0 : Fin 2)) *
        (1 + MvPowerSeries.X (1 : Fin 2))
theorem

formalLogOnePlusProductArgument_constantCoeff

L87 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_constantCoeff
Documentation

Establishes the identity MvPowerSeries.constantCoeff (formalLogOnePlusProductArgument A) = 0.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_constantCoeff
    (A : Type*) [CommRing A] :
    MvPowerSeries.constantCoeff (formalLogOnePlusProductArgument A) = 0
theorem

formalLogOnePlusProductArgument_hasSubst

L97 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_hasSubst
Documentation

The formal product argument has zero constant coefficient, so it admits substitution into the logarithm power series.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_hasSubst
    (A : Type*) [CommRing A] :
    PowerSeries.HasSubst (formalLogOnePlusProductArgument A)
theorem

formalLogOnePlusProductArgument_mulVariables_coeff

L108 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_mulVariables_coeff
Documentation

Establishes the identity MvPowerSeries.coeff e (MvPowerSeries.X (0 : Fin 2) * MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) = if e = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1 then 1 else 0.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgument_mulVariables_coeff
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e
        (MvPowerSeries.X (0 : Fin 2) *
          MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) =
      if e =
          Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1
      then 1 else 0 := by
  change MvPowerSeries.coeff e
      (MvPowerSeries.monomial (Finsupp.single (0 : Fin 2) 1) (1 : A) *
        MvPowerSeries.monomial (Finsupp.single (1 : Fin 2) 1) (1 : A)) =
    if e =
        Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1
    then 1 else 0
  rw [MvPowerSeries.monomial_mul_monomial]
  simp [MvPowerSeries.coeff_monomial]
theorem

formalLogOnePlusProductArgument_coeff

L130 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff
Documentation

Establishes the identity `MvPowerSeries.coeff e (formalLogOnePlusProductArgument A) = (if e = Finsupp.single (0 : Fin 2) 1 then 1 else 0) + (if e = Finsupp.single (1 : Fin 2) 1 then 1 else 0)

  • (if e = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1 then 1 else 0)`.
Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · full declaration
theorem formalLogOnePlusProductArgument_coeff
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e (formalLogOnePlusProductArgument A) =
      (if e = Finsupp.single (0 : Fin 2) 1 then 1 else 0) +
        (if e = Finsupp.single (1 : Fin 2) 1 then 1 else 0) +
          (if e =
              Finsupp.single (0 : Fin 2) 1 +
                Finsupp.single (1 : Fin 2) 1
            then 1 else 0) := by
  simp [formalLogOnePlusProductArgument, MvPowerSeries.coeff_X,
    formalLogOnePlusProductArgument_mulVariables_coeff]
theorem

formalLogOnePlusProductArgument_coeff_eq_zero_of_not_basic

L143 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_eq_zero_of_not_basic
Documentation

Establishes the identity MvPowerSeries.coeff e (formalLogOnePlusProductArgument A) = 0.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_eq_zero_of_not_basic
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ)
    (hleft : e ≠ Finsupp.single (0 : Fin 2) 1)
    (hright : e ≠ Finsupp.single (1 : Fin 2) 1)
    (hmixed :
      e ≠
        Finsupp.single (0 : Fin 2) 1 +
          Finsupp.single (1 : Fin 2) 1) :
    MvPowerSeries.coeff e (formalLogOnePlusProductArgument A) = 0
theorem

finsupp_fin_two_single_left_ne_single_right

L156 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_single_left_ne_single_right
Documentation

Establishes the inequality Finsupp.single (0 : Fin 2) 1 ≠ Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_single_left_ne_single_right :
    Finsupp.single (0 : Fin 2) 1 ≠ Finsupp.single (1 : Fin 2) 1
theorem

finsupp_fin_two_single_left_ne_mixed

L166 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_single_left_ne_mixed
Documentation

Establishes the inequality Finsupp.single (0 : Fin 2) 1 ≠ Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_single_left_ne_mixed :
    Finsupp.single (0 : Fin 2) 1 ≠
      Finsupp.single (0 : Fin 2) 1 +
        Finsupp.single (1 : Fin 2) 1
theorem

finsupp_fin_two_single_right_ne_mixed

L178 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_single_right_ne_mixed
Documentation

Establishes the inequality Finsupp.single (1 : Fin 2) 1 ≠ Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_single_right_ne_mixed :
    Finsupp.single (1 : Fin 2) 1 ≠
      Finsupp.single (0 : Fin 2) 1 +
        Finsupp.single (1 : Fin 2) 1
theorem

formalLogOnePlusProductArgument_coeff_single_left

L190 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_single_left
Documentation

Establishes the identity MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) 1) (formalLogOnePlusProductArgument A) = 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_single_left
    (A : Type*) [CommRing A] :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) 1)
        (formalLogOnePlusProductArgument A) = 1
theorem

formalLogOnePlusProductArgument_coeff_single_right

L201 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_single_right
Documentation

Establishes the identity MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) 1) (formalLogOnePlusProductArgument A) = 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_single_right
    (A : Type*) [CommRing A] :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) 1)
        (formalLogOnePlusProductArgument A) = 1
theorem

formalLogOnePlusProductArgument_coeff_mixed

L216 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_mixed
Documentation

Establishes the identity MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1) (formalLogOnePlusProductArgument A) = 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_mixed
    (A : Type*) [CommRing A] :
    MvPowerSeries.coeff
        (Finsupp.single (0 : Fin 2) 1 +
          Finsupp.single (1 : Fin 2) 1)
        (formalLogOnePlusProductArgument A) = 1
theorem

formalLogOnePlusProductArgument_coeff_ne_zero_left_coord_le_one

L236 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_ne_zero_left_coord_le_one
Documentation

Proves the bound e (0 : Fin 2) ≤ 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_ne_zero_left_coord_le_one
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ)
    (hcoeff : MvPowerSeries.coeff e
      (formalLogOnePlusProductArgument A) ≠ 0) :
    e (0 : Fin 2) ≤ 1
theorem

formalLogOnePlusProductArgument_coeff_ne_zero_right_coord_le_one

L263 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_ne_zero_right_coord_le_one
Documentation

Proves the bound e (1 : Fin 2) ≤ 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_ne_zero_right_coord_le_one
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ)
    (hcoeff : MvPowerSeries.coeff e
      (formalLogOnePlusProductArgument A) ≠ 0) :
    e (1 : Fin 2) ≤ 1
theorem

finsupp_fin_two_eq_zero_of_coords_eq_zero

L290 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_eq_zero_of_coords_eq_zero
Documentation

Establishes the identity e = 0.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_eq_zero_of_coords_eq_zero
    (e : Fin 2 →₀ ℕ)
    (hleft : e (0 : Fin 2) = 0) (hright : e (1 : Fin 2) = 0) :
    e = 0
theorem

finsupp_fin_two_eq_single_left_of_coords_eq

L298 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_eq_single_left_of_coords_eq
Documentation

Establishes the identity e = Finsupp.single (0 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_eq_single_left_of_coords_eq
    (e : Fin 2 →₀ ℕ)
    (hleft : e (0 : Fin 2) = 1) (hright : e (1 : Fin 2) = 0) :
    e = Finsupp.single (0 : Fin 2) 1
theorem

finsupp_fin_two_eq_single_right_of_coords_eq

L306 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_eq_single_right_of_coords_eq
Documentation

Establishes the identity e = Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_eq_single_right_of_coords_eq
    (e : Fin 2 →₀ ℕ)
    (hleft : e (0 : Fin 2) = 0) (hright : e (1 : Fin 2) = 1) :
    e = Finsupp.single (1 : Fin 2) 1
theorem

finsupp_fin_two_eq_mixed_of_coords_eq_one

L314 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.finsupp_fin_two_eq_mixed_of_coords_eq_one
Documentation

Establishes the identity e = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem finsupp_fin_two_eq_mixed_of_coords_eq_one
    (e : Fin 2 →₀ ℕ)
    (hleft : e (0 : Fin 2) = 1) (hright : e (1 : Fin 2) = 1) :
    e =
      Finsupp.single (0 : Fin 2) 1 +
        Finsupp.single (1 : Fin 2) 1
theorem

formalLogOnePlusProductArgument_coeff_ne_zero_eq_basic

L327 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_coeff_ne_zero_eq_basic
Documentation

Establishes the identity e = Finsupp.single (0 : Fin 2) 1 ∨ e = Finsupp.single (1 : Fin 2) 1 ∨ e = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_coeff_ne_zero_eq_basic
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ)
    (hcoeff : MvPowerSeries.coeff e
      (formalLogOnePlusProductArgument A) ≠ 0) :
    e = Finsupp.single (0 : Fin 2) 1 ∨
      e = Finsupp.single (1 : Fin 2) 1 ∨
        e =
          Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1
theorem

formalLogOnePlusProductArgument_pow_term_factor_eq_basic_of_prod_ne_zero

L367 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalLogOnePlusProductArgument_pow_term_factor_eq_basic_of_prod_ne_zero
Documentation

Establishes the identity l i = Finsupp.single (0 : Fin 2) 1 ∨ l i = Finsupp.single (1 : Fin 2) 1 ∨ l i = Finsupp.single (0 : Fin 2) 1 + Finsupp.single (1 : Fin 2) 1.

Source context 4 commands

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

noncomputable section
attribute [local instance] Classical.propDecidable
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
Lean source · statement
theorem formalLogOnePlusProductArgument_pow_term_factor_eq_basic_of_prod_ne_zero
    (A : Type*) [CommRing A] {q : ℕ}
    {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hprod :
      (∏ i ∈ Finset.range q,
        MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) ≠ 0)
    {i : ℕ} (hi : i ∈ Finset.range q) :
    l i = Finsupp.single (0 : Fin 2) 1 ∨
      l i = Finsupp.single (1 : Fin 2) 1 ∨
        l i =
          Finsupp.single (0 : Fin 2) 1 +
            Finsupp.single (1 : Fin 2) 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.