Commit 2023-03-17 14:06 87ede419

View on Github →

chore: forward port leanprover-community/mathlib#18575 (#2899) This somewhat re-ports the file from scratch (by manually cleaning up the mathport output to remove all the meta comments), as lots of workarounds were added in #2570 to deal with coercion issues. All proof changes are restoring the mathport proofs, except for small modifications to use simp [(foo)] instead of simp [foo] or simp (where foo was already a simp lemma). leanprover-community/mathlib#18575

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

modified theorem AffineMap.coeFn_injective

modified theorem AffineMap.coe_one

modified theorem AffineMap.coe_smul

modified def AffineMap.comp

modified def AffineMap.const

modified theorem AffineMap.decomp'

modified theorem AffineMap.decomp

modified theorem AffineMap.ext

modified def AffineMap.homothetyHom

deleted def AffineMap.id

modified def AffineMap.linearHom

modified def AffineMap.proj

modified def AffineMap.toConstProdLinearMap

added theorem AffineMap.toFun_eq_coe

modified structure AffineMap