Revision #1652 → #1811 · back to history
modifiedTrivial bundle of rank k281b4ad7bf4c
| Field | From #1652 | To #1811 |
|---|
| mathlib.module | Mathlib.Topology.FiberBundle.Constructions | Mathlib.Data.Bundle |
addedMöbius band as non-trivial line bundle51247d341c10
modifiedVector bundle morphism0b9ceeeeb04d
| Field | From #1652 | To #1811 |
|---|
| anchors | [{"section":"Vector bundle morphisms","snippet":"A morphism from the vector bundle"},{"type":"math_alttext","value":"{\\displaystyle g\\circ \\pi _{1}=\\pi _{2}\\circ f}"}] | — |
| provenance | ai | ai-moderated |
addedSection of tangent bundle is a vector field28ec0306262a
modifiedVector bundle metric2b8c87bdf57b
| Field | From #1652 | To #1811 |
|---|
| mathlib.decl | RiemannianBundle | Bundle.RiemannianBundle |
| note | `RiemannianBundle`/`IsContinuousRiemannianBundle` equip a real vector bundle with a continuous fiberwise inner product, i.e. a bundle metric. | `Bundle.RiemannianBundle`/`IsContinuousRiemannianBundle` equip a real vector bundle with a continuous fiberwise inner product, i.e. a bundle metric. |
modifiedK-theory group6ad97c328bfc
| Field | From #1652 | To #1811 |
|---|
| anchors | [{"section":"K-theory","snippet":"is defined as the abelian group generated by isomorphism classes"},{"type":"math_alttext","value":"{\\displaystyle 0\\to A\\to B\\to C\\to 0,}"},{"type":"math_alttext","value":"{\\displaystyle [B]=[A]+[C]}"}] | — |
| provenance | ai | ai-moderated |