Commit 2021-09-20 10:37 e29dfc19

View on Github →

chore(analysis/normed_space/finite_dimensional): restructure imports (#9289) Delays importing linear_algebra.finite_dimensional in the analysis/normed_space/ directory until it is really needed. This reduces the "long pole" of mathlib compilation by 3 minutes (out of 55).

Estimated changes

Modified src/analysis/normed_space/affine_isometry.lean

deleted theorem affine_isometry.coe_to_affine_isometry_equiv

deleted theorem affine_isometry.to_affine_isometry_equiv_apply

Modified src/analysis/normed_space/finite_dimension.lean

added theorem affine_isometry.coe_to_affine_isometry_equiv

added def affine_isometry.to_affine_isometry_equiv

added theorem affine_isometry.to_affine_isometry_equiv_apply

added theorem linear_isometry.coe_to_linear_isometry_equiv

added def linear_isometry.to_linear_isometry_equiv

added theorem linear_isometry.to_linear_isometry_equiv_apply

Modified src/analysis/normed_space/linear_isometry.lean

deleted theorem linear_isometry.coe_to_linear_isometry_equiv

deleted theorem linear_isometry.to_linear_isometry_equiv_apply