Revision #1367 → #2114 · back to history
modifiedPreservation of linear combinationsee03229d3d5e
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Module.LinearMap.Defs | Mathlib.Algebra.BigOperators.Group.Finset.Defs |
| note | Linear maps preserve finite sums (via `map_sum`) and scalar multiples (`map_smul`), hence preserve linear combinations. | Linear maps preserve finite sums (via `map_sum`) and scalar multiples (`LinearMap.map_smul`), hence preserve linear combinations. |
modifiedUnique map of given form is linear6d8e2926fb03
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Module.LinearMap.Defs | Mathlib.Algebra.Module.LinearMap.End |
modifiedLine through the originfaa2c189d173
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Algebra.Bilinear | Mathlib.LinearAlgebra.BilinearMap |
modifiedHomothety is linearf9915710617e
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Algebra.Bilinear | Mathlib.LinearAlgebra.BilinearMap |
modifiedIsometry on real normed spaces8a22b9781597
| Field | From #1367 | To #2114 |
|---|
| mathlib.match_kind | generalization | special_case |
| note | `LinearIsometry` formalizes norm-preserving linear maps between normed spaces. | `LinearIsometry` bundles norm-preserving linear maps, but the Wikipedia claim is the Mazur–Ulam-style converse ('an isometry sending 0 to 0 is linear'), which is the relevant direction here. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedDefinite integral is linear5af80902be1f
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Integral.IntervalIntegral | Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic |
modifiedComponent scaling is linearc36c4c4526d4
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Module.LinearMap.Defs | Mathlib.Algebra.Module.LinearMap.End |
modifiedLinear extension7061b172a30f
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | Basis.constr | Module.Basis.constr |
| note | Mathlib has `Basis.constr` to extend a function on a basis to a linear map, but no general 'linear extension of a function on a subset' definition matching the Wikipedia notion. | Mathlib has `Module.Basis.constr` to extend a function on a basis to a linear map, but no general 'linear extension of a function on a subset' definition matching the Wikipedia notion. |
modifiedLinearly independent set extensionc6faabcd79f7
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | Basis.constr | Module.Basis.constr |
| note | `Basis.constr` lets any function on a basis be linearly extended; together with extension of a linearly independent set to a basis, this gives the Wikipedia statement. | `Module.Basis.constr` lets any function on a basis be linearly extended; together with extension of a linearly independent set to a basis, this gives the Wikipedia statement. |
modifiedRotation by 90 degrees counterclockwise8ebedc52c522
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Analysis.Complex.Isometry | Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic |
modifiedRotation by angle θ53e1390769b9
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Analysis.Complex.Isometry | Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic |
modifiedScaling by 26ff186352fa7
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Algebra.Bilinear | Mathlib.LinearAlgebra.BilinearMap |
modifiedSet of linear maps forms a vector space52fa55b31782
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | LinearMap.instModule | LinearMap.module |
| note | Mathlib gives `M →ₛₗ[σ] N` a `Module` instance, making `Hom(V,W)` a vector space. | Mathlib gives `M →ₛₗ[σ] N` a `Module` instance via `LinearMap.module`, making `Hom(V,W)` a vector space. |
modifiedAutomorphism and automorphism groupa6b9771c4fd9
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.Algebra.Module.LinearMap.GeneralLinearGroup | Mathlib.LinearAlgebra.GeneralLinearGroup.Basic |
modifiedRank and nullitycd17badeb70e
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.Dimension.Constructions | Mathlib.LinearAlgebra.Dimension.LinearMap |
modifiedCokernel2c4ad85ceed0
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | Submodule.Quotient | Submodule.hasQuotient |
| mathlib.module | Mathlib.LinearAlgebra.Quotient.Basic | Mathlib.LinearAlgebra.Quotient.Defs |
| note | The cokernel is `M₂ ⧸ LinearMap.range f`, expressed using `Submodule` quotients; explicitly used in `Mathlib.Algebra.Module.Presentation.Cokernel`. | The cokernel is `M₂ ⧸ LinearMap.range f`, expressed using the `Submodule.hasQuotient` quotient construction. |
modifiedCokernel exact sequence6274bb1c4c62
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | ShortComplex.cokernelSequence | CategoryTheory.ShortComplex.Exact |
| note | Exact-sequence formalism (e.g., `ShortComplex`/`cokernelSequence`) covers this in general categorical setting; no direct Wikipedia-style statement for modules. | Exact-sequence formalism via `CategoryTheory.ShortComplex.Exact` covers this in the general categorical setting; no direct Wikipedia-style statement for modules. |
modifiedNilpotent, idempotent, scaling endomorphisms38e860ccbb11
| Field | From #1367 | To #2114 |
|---|
| mathlib.module | Mathlib.RingTheory.Nilpotent.Defs | Mathlib.Algebra.GroupWithZero.Basic |
modifiedContinuity equals boundednessc6f5d628daad
| Field | From #1367 | To #2114 |
|---|
| mathlib.decl | LinearMap.continuous_iff_isBounded | IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap |
| note | Mathlib's `isLinearMap_and_continuous_iff_isBoundedLinearMap` (and related `LinearMap.continuous_of_bound`) state continuity equivalent to boundedness. | `IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap` states that a function is linear and continuous iff it is a bounded linear map. |
addedLinear maps send subspaces to subspaces8f89d2d1820a
addedCategory of vector spaces / modules54e820e514d2
addedAutomorphism group as units of endomorphism ringccc4bdf6776a
addedAutomorphism group isomorphic to GLₙ07f5bdf6d168