Structures · Topology
Bundle.Pretrivialization.IsLinear
A mixin class for Pretrivialization, stating that a pretrivialization is fiberwise linear with
respect to given module structures on its fibers and the model fiber.
- Defined in
- Mathlib.Topology.VectorBundle.Basic
- Shape
- 2 explicit arguments · adds linear
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- Bundle.Pretrivialization.linearMapAt
- Bundle.Pretrivialization.symmₗ
- Bundle.Pretrivialization.symmₗ_apply
- Bundle.Pretrivialization.linearEquivAt
- Bundle.Pretrivialization.coe_linearMapAt
- Bundle.Pretrivialization.coe_linearMapAt_of_mem
- Bundle.Pretrivialization.IsLinear.linear
- Bundle.Pretrivialization.symmₗ_apply_of_notMem
- Bundle.Pretrivialization.linearMapAt_symmₗ
- Bundle.Pretrivialization.symmₗ_linearMapAt
- Bundle.Pretrivialization.linearMapAt_apply
- Bundle.Pretrivialization.linearEquivAt.congr_simp
- Bundle.Pretrivialization.linearEquivAt_symm_apply
- Bundle.Pretrivialization.symmₗ.congr_simp
- Bundle.Pretrivialization.linearMapAt_def_of_mem
- Bundle.Pretrivialization.linearMapAt.congr_simp
- Bundle.Pretrivialization.linear
- Bundle.Pretrivialization.linearEquivAt_apply
- Bundle.Pretrivialization.linearMapAt_def_of_notMem
- Bundle.Pretrivialization.linearMapAt_eq_zero
Ancestors0
No ancestors.