Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-19 11:16 e96bdfbd

View on Github →

chore(linear_algebra/affine_space/affine_subspace) add set_like instance (#18622) Needed for the port.

Estimated changes

Modified src/linear_algebra/affine_space/affine_subspace.lean

modified theorem affine_subspace.coe_injective

added theorem affine_subspace.ext

Modified src/linear_algebra/affine_space/pointwise.lean