English
The dualDistribEquiv is the preferred basis-dependent version of the isomorphism between Dual M ⊗ Dual N and Dual (M ⊗ N).
Русский
Dual Distrib Equiv — базис-зависимое эквивалентное отображение между Dual M ⊗ Dual N и Dual (M ⊗ N).
LaTeX
$$$$ dualDistribEquiv : Dual_R M \\otimes_R Dual_R N \\simeq_\\ell Dual_R (M \\otimes_R N). $$$$
Lean4
/-- The submodule `genEigenspace f μ k` for a linear map `f`, a scalar `μ`,
and a number `k : ℕ∞` is the kernel of `(f - μ • id) ^ k` if `k` is a natural number
(see Def 8.10 of [axler2015]), or the union of all these kernels if `k = ∞`.
A generalized eigenspace for some exponent `k` is contained in
the generalized eigenspace for exponents larger than `k`. -/
def genEigenspace (f : End R M) (μ : R) : ℕ∞ →o Submodule R M
where
toFun k := ⨆ l : ℕ, ⨆ _ : l ≤ k, LinearMap.ker ((f - μ • 1) ^ l)
monotone' _ _ hkl := biSup_mono fun _ hi ↦ hi.trans hkl
