Basics

This is the stem file (imported by every other file in this project). This file provides notation used throughout the project, some very basic lemmas, and a little bit of configuration.

Notation

@[reducible, inline]

abbrev Z2 : Type

The finite field on 2 elements; write Z2 for "value" type but Fin 2 for "indexing" type.

Equations

• Z2 = ZMod 2

@[reducible, inline]

abbrev Z3 : Type

The finite field on 3 elements; write Z3 for "value" type but Fin 3 for "indexing" type.

Equations

• Z3 = ZMod 3

def «term_ᕃ_» : Lean.TrailingParserDescr

Roughly speaking a ᕃ A is A ∪ {a}.

Equations

• «term_ᕃ_» = Lean.ParserDescr.trailingNode `«term_ᕃ_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᕃ ") (Lean.ParserDescr.cat `term 66))

def «term_⫗_» : Lean.TrailingParserDescr

Writing X ⫗ Y is slightly more general than writing X ∩ Y = ∅.

Equations

• «term_⫗_» = Lean.ParserDescr.trailingNode `«term_⫗_» 61 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⫗ ") (Lean.ParserDescr.cat `term 62))

def «term_.→» : Lean.TrailingParserDescr

The left-to-right direction of ↔.

Equations

• «term_.→» = Lean.ParserDescr.trailingNode `«term_.→» 1024 1024 (Lean.ParserDescr.symbol ".→")

def «term_.←» : Lean.TrailingParserDescr

The right-to-left direction of ↔.

Equations

• «term_.←» = Lean.ParserDescr.trailingNode `«term_.←» 1024 1024 (Lean.ParserDescr.symbol ".←")

def «term↓_» : Lean.ParserDescr

Writing ↓t is slightly more general than writing Function.const _ t.

Equations

• «term↓_» = Lean.ParserDescr.node `«term↓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↓") (Lean.ParserDescr.cat `term 1023))

def «term#_» : Lean.ParserDescr

We denote the cardinality of a Fintype the same way the cardinality of a Finset is denoted.

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

def «term_.≃» : Lean.TrailingParserDescr

Canonical bijection between subtypes corresponding to equal sets.

Equations

• «term_.≃» = Lean.ParserDescr.trailingNode `«term_.≃» 1024 1024 (Lean.ParserDescr.symbol ".≃")

def «term=.≃» : Lean.ParserDescr

The trivial bijection (identity).

Equations

• «term=.≃» = Lean.ParserDescr.node `«term=.≃» 1024 (Lean.ParserDescr.symbol "=.≃")

def «term◩_» : Lean.ParserDescr

The "left" or "top" variant.

Equations

• «term◩_» = Lean.ParserDescr.node `«term◩_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◩") (Lean.ParserDescr.cat `term 1024))

def «term◪_» : Lean.ParserDescr

The "right" or "bottom" variant.

Equations

• «term◪_» = Lean.ParserDescr.node `«term◪_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◪") (Lean.ParserDescr.cat `term 1024))

def «term_⊟_» : Lean.TrailingParserDescr

Glue rows of two matrices.

Equations

• «term_⊟_» = Lean.ParserDescr.trailingNode `«term_⊟_» 63 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟ ") (Lean.ParserDescr.cat `term 64))

def «term_◫_» : Lean.TrailingParserDescr

Glue cols of two matrices.

Equations

• «term_◫_» = Lean.ParserDescr.trailingNode `«term_◫_» 63 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◫ ") (Lean.ParserDescr.cat `term 64))

def «term⊞» : Lean.ParserDescr

Glue four matrices into one block matrix.

Equations

• «term⊞» = Lean.ParserDescr.node `«term⊞» 1024 (Lean.ParserDescr.symbol "⊞ ")

def «term▬_» : Lean.ParserDescr

Convert vector to a single-row matrix.

Equations

• «term▬_» = Lean.ParserDescr.node `«term▬_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▬") (Lean.ParserDescr.cat `term 81))

def «term▮_» : Lean.ParserDescr

Convert vector to a single-col matrix.

Equations

• «term▮_» = Lean.ParserDescr.node `«term▮_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▮") (Lean.ParserDescr.cat `term 81))

@[reducible, inline]

abbrev outerProduct {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Mul α] (c : X → α) (r : Y → α) : Matrix X Y α

Outer product of two vectors (the column vector comes on left; the row vector comes on right).

Equations

• c ⊗ r = Matrix.of fun (i : X) (j : Y) => c i * r j

def «term_⊗_» : Lean.TrailingParserDescr

Outer product of two vectors (the column vector comes on left; the row vector comes on right).

Equations

• «term_⊗_» = Lean.ParserDescr.trailingNode `«term_⊗_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 68))

@[reducible, inline]

abbrev entrywiseProduct {X : Type u_1} {Y : Type u_2} {α : Type u_3} {β : Type u_4} [SMul α β] (A : Matrix X Y α) (B : Matrix X Y β) : Matrix X Y β

Element-wise product of two matrices (rarely used).

Equations

• A ⊡ B = Matrix.of fun (i : X) (j : Y) => A i j • B i j

def «term_⊡_» : Lean.TrailingParserDescr

Element-wise product of two matrices (rarely used).

Equations

• «term_⊡_» = Lean.ParserDescr.trailingNode `«term_⊡_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ ") (Lean.ParserDescr.cat `term 66))

@[reducible, inline]

abbrev Function.range {α : Type u_1} {ι : Type u_2} (f : ι → α) : Set α

The set of possible outputs of a function.

Equations

• f.range = Set.range f

def Function.range_unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Function.support_unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

Basic stuff

theorem Function.range_eq {α : Type u_1} {ι : Type} (f : ι → α) : f.range = {a : α | ∃ (i : ι), f i = a}

theorem dite_of_true {α : Type u_1} {P : Prop} [Decidable P] (p : P) {f : P → α} {a : α} : (if hp : P then f hp else a) = f p

theorem dite_of_false {α : Type u_1} {P : Prop} [Decidable P] (p : ¬P) {f : P → α} {a : α} : (if hp : P then f hp else a) = a

@[reducible, inline]

abbrev Equiv.leftCongr {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} (e : ι₁ ≃ ι₂) : ι₁ ⊕ α ≃ ι₂ ⊕ α

Equations

• e.leftCongr = e.sumCongr (Equiv.refl α)

@[reducible, inline]

abbrev Equiv.rightCongr {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} (e : ι₁ ≃ ι₂) : α ⊕ ι₁ ≃ α ⊕ ι₂

Equations

• e.rightCongr = (Equiv.refl α).sumCongr e

@[simp]

theorem Equiv.image_symm_apply {α : Type u_1} {β : Type u_2} {X : Set α} (e : α ≃ β) (x : ↑X) : (e.image X).symm ⟨e ↑x, ⋯⟩ = x

theorem Finset.sum_of_single_nonzero {α : Type u_1} {ι : Type u_2} (s : Finset ι) [AddCommMonoid α] (f : ι → α) (a : ι) (ha : a ∈ s) (hf : ∀ i ∈ s, i ≠ a → f i = 0) : s.sum f = f a

theorem fintype_sum_of_single_nonzero {α : Type u_1} {ι : Type u_2} [Fintype ι] [AddCommMonoid α] (f : ι → α) (a : ι) (hf : ∀ (i : ι), i ≠ a → f i = 0) : Finset.univ.sum f = f a

theorem sum_elem_of_single_nonzero {α : Type u_1} {ι : Type u_2} [AddCommMonoid α] {f : ι → α} {S : Set ι} [Fintype ↑S] {a : ι} (haS : a ∈ S) (hf : ∀ (i : ι), i ≠ a → f i = 0) : ∑ i : ↑S, f ↑i = f a

theorem sum_over_fin_succ_of_only_zeroth_nonzero {α : Type u_1} {n : ℕ} [AddCommMonoid α] {f : Fin n.succ → α} (hf : ∀ (i : Fin n.succ), i ≠ 0 → f i = 0) : Finset.univ.sum f = f 0

Aesop modifiers

def tacticAesopnt : Lean.ParserDescr

Nonterminal aesop (dangerous).

Equations

• tacticAesopnt = Lean.ParserDescr.node `tacticAesopnt 1024 (Lean.ParserDescr.nonReservedSymbol "aesopnt" false)