Mathlib.ModelTheory.Algebra.Ring.Basic._auxLemma.1
theorem Mathlib.ModelTheory.Algebra.Ring.Basic._auxLemma.1 :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} {P : ((i : Fin (n + 1)) → α i) → Prop},
(∀ (x : (i : Fin (n + 1)) → α i), P x) = ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (Fin.cons a v)
This theorem states that for any natural number `n`, any dependent type `α` indexed by `Fin (n + 1)`, and any property `P` that takes a function from `Fin (n + 1)` to `α` and returns a proposition, the property `P` holds for all such functions if and only if it holds for all functions constructed by the `Fin.cons` method given any initial element `a : α 0` and a function `v : (i : Fin n) → α (Fin.succ i)`. In other words, a property holds for all functions from `Fin (n + 1)` to `α` if it holds for all functions formed by prepending an element to a function from `Fin n` to `α`.
More concisely: For any natural number $n$, property $P$ on functions from $Fin(n+1)$ to a type $\alpha$, and given any initial element $a : \alpha 0$ and function $v : Fin(n) \to \alpha$, $P$ holds for all functions if and only if it holds for functions constructed by appending $a$ to functions from $Fin(n)$ using $Fin.cons$.
|
FirstOrder.Ring.CompatibleRing.funMap_mul
theorem FirstOrder.Ring.CompatibleRing.funMap_mul :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
[self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2 → R),
FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1
The theorem `FirstOrder.Ring.CompatibleRing.funMap_mul` states that for any type `R` with operations `Add`, `Mul`, `Neg`, `One` and `Zero`, and for which a `FirstOrder.Ring.CompatibleRing` structure is defined, the interpretation of the multiplication function symbol in the language of rings is equivalent to the standard multiplication of the elements of `R`. More concretely, if `x` is a function from a two-element finite set to `R`, the interpretation of the multiplication function symbol applied to `x` is the same as the result of multiplying `x 0` by `x 1` in `R`.
More concisely: For any `FirstOrder.Ring.CompatibleRing` `R` and function `x` from a two-element finite set to `R`, the interpretation of the multiplication operation on `x` in the language of rings equals the standard multiplication of `x(0)` and `x(1)` in `R`.
|
FirstOrder.Ring.CompatibleRing.funMap_neg
theorem FirstOrder.Ring.CompatibleRing.funMap_neg :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
[self : FirstOrder.Ring.CompatibleRing R] (x : Fin 1 → R),
FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0
This theorem states that for any type `R` with addition, multiplication, negation, identity element (one), and a zero element, and satisfying the properties of a compatible ring in FirstOrder logic, the negation operation in the `FirstOrder.Language.Structure` is the same as the negation given by the `Neg` instance. More specifically, given a function `x` from a 1-dimensional finite set to `R`, applying the function map of the negation function `FirstOrder.Ring.negFunc` to `x` is equivalent to applying the negation to the element `x 0` in `R`.
More concisely: For any function `x` from a finite set to a ring `R` in First-Order logic, the function map of the negation function in the ring structure is equivalent to applying the additive negation to the value `x 0` in `R`.
|
FirstOrder.Ring.CompatibleRing.funMap_one
theorem FirstOrder.Ring.CompatibleRing.funMap_one :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
[self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0 → R),
FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1
The theorem `FirstOrder.Ring.CompatibleRing.funMap_one` asserts that for any given ring `R` (which supports addition, multiplication, negation, and has defined elements for one and zero), and for any function from `Fin 0` to `R`, the interpretation of the constant `1` in the `Language.ring.Structure` is the same as the constant given by the `One` instance. In other words, when the function `FirstOrder.Language.Structure.funMap` is applied to the function symbol `FirstOrder.Ring.oneFunc` and an arbitrary function from `Fin 0` to `R`, it always produces the constant `1` in the ring `R`.
More concisely: For any ring `R` and function `f : Fin 0 → R`, `FirstOrder.Language.Structure.funMap (FirstOrder.Ring.oneFunc) f = 1_R`.
|
FirstOrder.Ring.CompatibleRing.funMap_zero
theorem FirstOrder.Ring.CompatibleRing.funMap_zero :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
[self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0 → R),
FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0
This theorem states that for any ring `R` with the operations of addition, multiplication, negation, and the constant values one and zero, and any function `x` from a 0-dimensional finite set into `R`, the interpretation of the zero function symbol in the first order language structure of the ring is equal to the zero of that ring. In other words, the specific zero function symbol, as defined in the structure of a first order language for rings, maps to the actual zero of the ring `R`.
More concisely: For any ring `R` and any function `x` from a 0-dimensional finite set into `R`, the constant function with value 0 from the set to `R`, interpreted as a term in the first-order language of rings, equals the additive identity (zero) of `R`.
|
FirstOrder.Ring.CompatibleRing.funMap_add
theorem FirstOrder.Ring.CompatibleRing.funMap_add :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
[self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2 → R),
FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1
The theorem `FirstOrder.Ring.CompatibleRing.funMap_add` states that for any type `R` which has operations of addition, multiplication, negation, and distinct elements representing one and zero, and is a structure compatible with a ring in first-order language, the interpretation of the addition function symbol in the ring language structure is the same as the standard addition operation in `R`. Specifically, when applied to a function `x` from a finite set of size 2 to `R`, it equates the result of the function symbol map on the `addFunc` (which represents addition in the ring language) and `x` to the addition of `x` at 0 and `x` at 1.
More concisely: For any first-order structure `R` with operations of addition, multiplication, negation, and distinct elements representing one and zero, the function symbol for addition in the ring language interprets as the standard addition operation in `R`.
|
Mathlib.ModelTheory.Algebra.Ring.Basic._auxLemma.2
theorem Mathlib.ModelTheory.Algebra.Ring.Basic._auxLemma.2 :
∀ {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop}, (∀ (x : (i : Fin 0) → α i), P x) = P finZeroElim := by
sorry
This theorem, named `Mathlib.ModelTheory.Algebra.Ring.Basic._auxLemma.2`, states that for any dependent type `α` indexed by `Fin 0` (the type representing the empty set) and for any property `P` that holds for any function from `Fin 0` to `α`, asserting that `P` holds for all such functions is equivalent to asserting that `P` holds for the specific function `finZeroElim`. The function `finZeroElim` is an elimination principle for `Fin 0`, meaning it is a function from `Fin 0` to any type which is inevitably the empty function, as `Fin 0` has no elements.
More concisely: For any property `P` and dependent type `α` indexed by `Fin 0`, asserting that `P` holds for all functions from `Fin 0` to `α` is equivalent to asserting that `P` holds for the empty function `finZeroElim` from `Fin 0` to `α`.
|