Structures · Topology
Bundle.Trivialization.IsLinear
A mixin class for Bundle.Trivialization, stating that a trivialization 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 by78
- Bundle.Trivialization.coordChangeL
- Bundle.Trivialization.continuousLinearMapAt
- Bundle.Trivialization.symmL
- Bundle.Trivialization.continuousLinearEquivAt
- Bundle.Trivialization.linearMapAt
- Bundle.Trivialization.symmL_apply
- Bundle.Trivialization.continuousLinearMapAt_apply
- Bundle.Trivialization.coe_linearMapAt_of_mem
- Bundle.Trivialization.linearEquivAt
- Bundle.Trivialization.continuousLinearEquivAt_apply
- Bundle.Trivialization.continuousLinearEquivAt_symm_apply
- Bundle.Trivialization.coordChangeL_apply
- Bundle.Trivialization.symmₗ
- Bundle.Trivialization.linear
- Bundle.Trivialization.coordChangeL_apply'
- Bundle.Pretrivialization.continuousLinearMapCoordChange
- Bundle.Pretrivialization.continuousAlternatingMap
- Bundle.Pretrivialization.continuousLinearMap
- Bundle.Trivialization.coe_continuousLinearEquivAt_eq
- Bundle.Trivialization.zeroSection
- Bundle.Trivialization.coe_linearMapAt
- Bundle.Trivialization.coe_coordChangeL
- Bundle.Pretrivialization.continuousAlternatingMapCoordChange
- Bundle.Trivialization.mk_coordChangeL
- Bundle.Trivialization.symmₗ_apply
- Bundle.Pretrivialization.continuousAlternatingMap_symm_apply'
- Bundle.Trivialization.linearMapAt_symmₗ
- Bundle.Trivialization.symm_coordChangeL
- Bundle.Trivialization.coe_coordChangeL'
- Bundle.Pretrivialization.continuousLinearMap_symm_apply'
- Bundle.Trivialization.prod_apply'
- Bundle.Trivialization.symmₗ_linearMapAt
- Bundle.Trivialization.symm_continuousLinearEquivAt_eq
- Bundle.Trivialization.apply_eq_prod_continuousLinearEquivAt
- Bundle.Trivialization.IsLinear.linear
- Bundle.Trivialization.apply_symm_apply_eq_coordChangeL
- Bundle.Trivialization.symmₗ.congr_simp
- Bundle.Trivialization.continuousLinearMapAt_apply_of_mem
- Bundle.Trivialization.coe_symmₗ
- Bundle.Trivialization.linearMapAt_apply
- Bundle.Trivialization.linearMapAt.congr_simp
- Bundle.Trivialization.linearMapAt_symm
- Bundle.Trivialization.toPretrivialization.isLinear
- Bundle.Trivialization.coordChangeL_symm_apply
- Bundle.Pretrivialization.continuousLinearMap_symm_apply
- Bundle.Pretrivialization.continuousAlternatingMap.congr_simp
- Bundle.Trivialization.linearEquivAt_symm_apply
- Bundle.Trivialization.coe_continuousLinearEquivAt_eq'
- Bundle.Trivialization.symmL.congr_simp
- Bundle.Trivialization.continuousLinearMapAt.congr_simp
Ancestors0
No ancestors.