affine_isometry): `base_at` construction
#8837

Open

feat(algebra/add_torsor, linear_algebra/affine_space/affine_equiv, analysis/normed_space/affine_isometry): `base_at` construction #8837

hrmacbeth wants to merge 14 commits into master from affine-equiv-lemmas

basics

cbaf9126

const_vadd lemmas

9186e58b

isometry_equiv lemmas

90f81726

hrmacbeth added awaiting-review

adjust lemma selection

83b68e09

golf

60cc4464

golf

513b0cc7

golf

40fb979c

trim lemma selection

418c71db

namespace

894cf295

docstring error

ca77362c

namespace

f922c1ee

github-actions added merge-conflict

Merge remote-tracking branch 'origin/master' into affine-equiv-lemmas

6c2382f7

github-actions removed merge-conflict

fix

f1c5d006

fix

7de147c0

urkud commented on 2021-09-11

jcommelin approved these changes on 2021-09-30

eric-wieser commented on 2021-09-30

kim-em added awaiting-author

sgouezel removed awaiting-review

github-actions added merge-conflict

kim-em added too-late

Reviewers

jcommelin

eric-wieser

urkud

Assignees

No one assigned

Labels

awaiting-author merge-conflict too-late

Milestone

No milestone

mathlib3 feat(algebra/add_torsor, linear_algebra/affine_space/affine_equiv, analysis/normed_space/affine_isometry): `base_at` construction #8837 Open

feat(algebra/add_torsor, linear_algebra/affine_space/affine_equiv, analysis/normed_space/affine_isometry): `base_at` construction #8837

mathlib3
feat(algebra/add_torsor, linear_algebra/affine_space/affine_equiv, analysis/normed_space/affine_isometry): `base_at` construction
#8837

Open