Source indexedlemma · leanprover/lean4:v4.33.0-rc1

dimension_of_shift

PFR.WeakPFR · PFR/WeakPFR.lean:802 to 817

Source documentation

In fact one has equality here, but this is trickier to prove and not needed for the argument.

Exact Lean statement

lemma dimension_of_shift {G : Type*} [AddCommGroup G] {H : AddSubgroup G}
    (A : Set H) (x : G) :
    AffineSpace.finrank ℤ ((fun a : H ↦ (a : G) + x) '' A) = AffineSpace.finrank ℤ A

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dimension_of_shift {G : Type*} [AddCommGroup G] {H : AddSubgroup G}    (A : Set H) (x : G) :    AffineSpace.finrank ℤ ((fun a : H ↦ (a : G) + x) '' A) = AffineSpace.finrank ℤ A := by  classical  calc    _ = AffineSpace.finrank ℤ (x +ᵥ Subtype.val '' A) := by      simp [← image_vadd, image_image, add_comm]    _ = AffineSpace.finrank ℤ (Subtype.val '' A) := by rw [AffineSpace.finrank_vadd_set]    _ = ((vectorSpan ℤ A).map H.subtype.toIntLinearMap).finrank := by      simp only [AffineSpace.finrank, vectorSpan, Submodule.map_span,        AddMonoidHom.coe_toIntLinearMap, AddSubgroup.subtype_apply]      congr! 2      symm      exact image_image2_distrib fun _ _ ↦ rfl    _ = AffineSpace.finrank ℤ A :=      (Submodule.equivMapOfInjective _ Subtype.val_injective _).symm.finrank_eq