Mathlib v3 is deprecated. Go to Mathlib v4

Theorem affine_subspace.subtypeₐᵢ_linear

Modification history

2022-09-23 08:22

src/analysis/normed_space/affine_isometry.lean

feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573) …

Added affine_subspace.subtypeₐᵢ_linear View on Github →