mathlib3

d55a93d8 - feat(linear_algebra/affine_space/affine_subspace): induction principle (#17520)

feat(linear_algebra/affine_space/affine_subspace): induction principle (#17520) Proves affine analogues of `submodule.span_induction'`, `submodule.span_induction'` and `submodule.span_span_coe_preimage`.