Mathlib.LinearAlgebra.Prod._auxLemma.1
theorem Mathlib.LinearAlgebra.Prod._auxLemma.1 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F}
{y : M}, (y ∈ LinearMap.ker f) = (f y = 0)
The theorem `Mathlib.LinearAlgebra.Prod._auxLemma.1` states that for any semirings `R` and `R₂`, additively commutative monoids `M` and `M₂`, `R`-module `M`, `R₂`-module `M₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` which is "function-like" from `M` to `M₂`, and which is a semilinear map from `M` to `M₂` over the ring homomorphism `τ₁₂`, and for any element `f` of type `F` and `y` of type `M`, the statement `y` is in the kernel of `f` is equivalent to the statement that applying `f` to `y` yields the zero element of `M₂`. In other words, an element `y` lies in the kernel of the semilinear map `f` if and only if `f(y)` equals zero.
More concisely: For any semirings R and R₂, additively commutative monoids M and M₂, R-module M, R₂-module M₂, a ring homomorphism τ₁₂ from R to R₂, a semilinear map F from M to M₂ over τ₁₂, and any y in M, the element y lies in the kernel of F if and only if F(y) = 0 in M₂.
|
Mathlib.LinearAlgebra.Prod._auxLemma.30
theorem Mathlib.LinearAlgebra.Prod._auxLemma.30 : ∀ {a : Prop}, (a → a) = True
This theorem, `Mathlib.LinearAlgebra.Prod._auxLemma.30`, states that for any proposition `a`, the statement "`a` implies `a`" is always true. In other words, if any proposition is true, then it indeed implies itself. This is a fundamental law of logic known as reflexivity.
More concisely: For any proposition `a`, `a` implies `a`.
|
LinearMap.prod_ext
theorem LinearMap.prod_ext :
∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
[inst_6 : Module R M₃] {f g : M × M₂ →ₗ[R] M₃},
f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ →
f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂ → f = g
The theorem `LinearMap.prod_ext` states that for any semiring `R` and additive commutative monoids `M`, `M₂`, `M₃`, where `M`, `M₂`, `M₃` are also `R`-modules, if we have two linear maps `f` and `g` from the cartesian product of `M` and `M₂` to `M₃`, and if the composition of `f` and `g` with the left injection linear map is equal, and the composition of `f` and `g` with the right injection linear map is also equal, then `f` and `g` are equal. This theorem allows us to split the equality of linear maps from a product into linear maps over each component, aiding us to apply lemmas specific to the individual linear maps.
More concisely: If two linear maps from the product of two additive commutative monoids (also R-modules) to a third R-module have equal compositions with the left and right injection linear maps, then they are equal.
|
Mathlib.LinearAlgebra.Prod._auxLemma.25
theorem Mathlib.LinearAlgebra.Prod._auxLemma.25 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem, `Mathlib.LinearAlgebra.Prod._auxLemma.25`, states that for any proposition `b` and for any type `α` that is nonempty (meaning there exists at least one element of this type), the function type `(α → b)` is equivalent to `b`. That means, the truth value of `b` does not depend on the specific element of `α` we choose, i.e., every function from `α` to `b` yields the same result for all elements of `α`.
More concisely: For any nonempty type `α` and proposition `b`, the type of functions from `α` to `b` is equivalent to `b`.
|
Mathlib.LinearAlgebra.Prod._auxLemma.27
theorem Mathlib.LinearAlgebra.Prod._auxLemma.27 :
∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, a = a' ∧ p a) = p a'
This theorem states that for any type `α`, any predicate `p` over this type, and any value `a'` of this type, there exists `a` such that `a` equals `a'` and `p` is true for `a` if and only if `p` is true for `a'`. In other words, the existence of an element satisfying some property is equivalent to that property being true for a specific element.
More concisely: For any type `α`, predicate `p` over `α`, and value `a'` in `α`, there exists `a` in `α` such that `a = a'` if and only if `p(a) ↔ p(a')`.
|
LinearMap.range_prod_eq
theorem LinearMap.range_prod_eq :
∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
[inst_6 : Module R M₃] {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃},
LinearMap.ker f ⊔ LinearMap.ker g = ⊤ →
LinearMap.range (f.prod g) = (LinearMap.range f).prod (LinearMap.range g)
This theorem states that for any two linear maps `f` and `g` from a module `M` over a ring `R` to modules `M₂` and `M₃` over `R`, respectively, if the union of the kernels of `f` and `g` spans the entire module `M` (represented by `⊤`), then the range of the product of `f` and `g` is equal to the product of the ranges of `f` and `g`. The product of `f` and `g` is a function that maps each element in the domain to a pair in the codomain, formed by the images of the element under `f` and `g`.
More concisely: If linear maps `f : M → M₂` and `g : M → M₃` from a module `M` over a ring `R` have kernels whose sum is equal to the module `M`, then the range of their product `f ∘ g` is equal to the product of the ranges of `f` and `g`.
|
Mathlib.LinearAlgebra.Prod._auxLemma.2
theorem Mathlib.LinearAlgebra.Prod._auxLemma.2 :
∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {F : Type u_11} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂]
[inst_8 : RingHomSurjective τ₁₂] {f : F} {x : M₂}, (x ∈ LinearMap.range f) = ∃ y, f y = x
The theorem `Mathlib.LinearAlgebra.Prod._auxLemma.2` in Lean 4 states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, `R`-module structure on `M`, `R₂`-module structure on `M₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` which behaves like a function from `M` to `M₂`, a semilinear map structure on `F` with respect to the ring homomorphism `τ₁₂`, and the assumption that `τ₁₂` is surjective. If we consider any `f` of type `F` and `x` of type `M₂`, then `x` is in the range of the linear map `f` if and only if there exists `y` such that `f y = x`. In other words, an element is in the range of a linear map if and only if it is the image of some element under the map.
More concisely: For any surjective ring homomorphism τ₁₂ from semiring R to R₂, and semilinear map F from an additive commutative monoid M to an R₂-module M₂, an element x of M₂ is in the range of F if and only if there exists y in M such that F(y) = x.
|
Mathlib.LinearAlgebra.Prod._auxLemma.18
theorem Mathlib.LinearAlgebra.Prod._auxLemma.18 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, from the Mathlib Linear Algebra Product Auxiliary Lemma 18, states that for any set of elements (`α`), and for any two elements (`a` and `b`) from that set, the statement that `a` equals `b` is equivalent to the statement that `b` equals `a`. In other words, it asserts the symmetry of equality in any set: if `a` is equal to `b`, then `b` is also equal to `a`.
More concisely: For all sets `α` and all `a, b` in `α`, `a = b` if and only if `b = a`.
|
Mathlib.LinearAlgebra.Prod._auxLemma.24
theorem Mathlib.LinearAlgebra.Prod._auxLemma.24 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) = ∀ (a : α) (b : β), p (a, b)
This theorem, from the Mathlib Linear Algebra library in Lean, states that for any types `α` and `β`, and any property `p` that applies to pairs of values (one from `α`, one from `β`), the assertion that `p` holds for all pairs is equivalent to the assertion that for every individual value `a` from type `α` and `b` from type `β`, `p` holds for the pair `(a, b)`. In other words, we can express a universal claim about all pairs either by quantifying over all pairs directly or by separately quantifying over all elements of the two types that make up the pairs.
More concisely: For any types `α` and `β` and property `p` on pairs `(α × β)`, the following are equivalent: `∀ (a : α) (b : β), p a b` and `∀ (a : α) (b : β), p (a, b)`.
|
Mathlib.LinearAlgebra.Prod._auxLemma.6
theorem Mathlib.LinearAlgebra.Prod._auxLemma.6 :
∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
(x ∈ ⊥) = (x = 0)
This theorem, named "Mathlib.LinearAlgebra.Prod._auxLemma.6," states that for any semiring `R`, an additively commutative monoid `M` and a module `M` over `R`, an element `x` of `M` belongs to the bottom module (denoted as `⊥` in Lean) if and only if `x` is equal to the zero element of `M`. In simple terms, in the context of linear algebra, the theorem says that an element belongs to the zero submodule if and only if it is the zero vector.
More concisely: For any semiring R, additively commutative monoid M, and R-module M, an element x of M belongs to the bottom module if and only if x is the additive identity of M.
|
Mathlib.LinearAlgebra.Prod._auxLemma.26
theorem Mathlib.LinearAlgebra.Prod._auxLemma.26 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∃ x, p x) = ∃ a b, p (a, b)
This theorem from the `Mathlib.LinearAlgebra.Prod` module, named `_auxLemma.26`, states that for any types `α` and `β`, and a property `p` that takes a pair from `α` and `β`, the existence of a pair `(a, b)` such that the property `p` holds is equivalent to the existence of an element `x` such that the property holds when `x` is considered as a pair. In other words, it establishes the equivalence of the two existential quantifications when the elements are pairs, making it easier to reason about properties that involve pairs of elements from arbitrary types.
More concisely: For any types `α` and `β` and property `p` on pairs from `α × β`, the existence of `(a, b)` such that `p(a, b)` holds is equivalent to the existence of `x` such that `p(x)` holds when `x` is considered as a pair.
|
Mathlib.LinearAlgebra.Prod._auxLemma.23
theorem Mathlib.LinearAlgebra.Prod._auxLemma.23 :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop},
(∀ (x : { a // p a }), q x) = ∀ (a : α) (b : p a), q ⟨a, b⟩
This theorem states that for any type `α` and predicates `p` and `q` such that `q` applies to elements of type `α` satisfying `p`, the statement "for all elements `x` of type `α` satisfying `p`, `q` holds" is equivalent to the statement "for all elements `a` of type `α` and `b` such that `p` holds for `a`, `q` holds for the subtype `{ val := a, property := b }`." Essentially, it's a formalization of substituting `x` with `{ val := a, property := b }` within the context of universal quantifiers and subtype definitions.
More concisely: For any type `α`, predicates `p` and `q`, if `q` holds for all elements `x` of type `α` satisfying `p`, then `q` holds for all elements of the subtype `{a : α | p a}`.
|
LinearMap.tunnelAux_injective
theorem LinearMap.tunnelAux_injective :
∀ {R : Type u} {M : Type v} [inst : Ring R] {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M × N →ₗ[R] M),
Function.Injective ⇑f → ∀ (Kφ : (K : Submodule R M) × ↥K ≃ₗ[R] M), Function.Injective ⇑(f.tunnelAux Kφ)
The theorem `LinearMap.tunnelAux_injective` states that for any ring `R` and its modules `M` and `N`, given a linear map `f` from the cartesian product of `M` and `N` to `M`, if `f` is injective, then for any isomorphism `Kφ` between a pair consisting of a submodule `K` of `M` and an element of `K`, and `M`, the function obtained by applying `LinearMap.tunnelAux` to `f` and `Kφ` is also injective.
More concisely: If `f` is an injective linear map from `M × N` to `M`, for any submodule `K` of `M` and isomorphism `Kφ` between `K` and an element of `M`, the linear map obtained by applying `LinearMap.tunnelAux` to `f` and `Kφ` is also injective.
|
Mathlib.LinearAlgebra.Prod._auxLemma.19
theorem Mathlib.LinearAlgebra.Prod._auxLemma.19 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{σ₁₂ : R →+* R₂} [inst_6 : RingHomSurjective σ₁₂] {F : Type u_9} [inst_7 : FunLike F M M₂]
[inst_8 : SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂},
(x ∈ Submodule.map f p) = ∃ y ∈ p, f y = x
The theorem `Mathlib.LinearAlgebra.Prod._auxLemma.19` in natural language states that:
For any two semirings `R` and `R₂`, two additively commutative monoids `M` and `M₂`, modules `M` and `M₂` over `R` and `R₂` respectively, a surjective ring homomorphism `σ₁₂` from `R` to `R₂`, a function-like `F` from `M` to `M₂`, a semilinear map class `F σ₁₂ M M₂`, a function `f` of type `F`, a submodule `p` of `M`, and an element `x` of `M₂`, the theorem asserts that `x` is in the image of the submodule `p` under the function `f` if and only if there exists an element `y` in `p` such that `f y` equals `x`.
This theorem describes a condition for an element to be in the image of a submodule under a function (which behaves like a semilinear map), and it's fundamental for understanding mappings between different algebraic structures in linear algebra.
More concisely: For a surjective ring homomorphism σ₁₂ from semirings R to R₂, a semilinear map F from module M over R to module M₂ over R₂, and a submodule p of M, an element x in M₂ is in the image of p under F if and only if there exists y in p such that F(y) = x.
|