English
The equality domDomCongr σ f = domDomCongr σ g implies f = g; conversely, f=g implies domDomCongr σ f = domDomCongr σ g.
Русский
Равенство domDomCongr σ f и domDomCongr σ g следует влечь за собой f=g, и наоборот.
LaTeX
$$Eq (AlternatingMap.domDomCongr σ f) (AlternatingMap.domDomCongr σ g) ↔ f = g$$
Lean4
/-- If the arguments are linearly dependent then the result is `0`. -/
theorem map_linearDependent {K : Type*} [Ring K] {M : Type*} [AddCommGroup M] [Module K M] {N : Type*} [AddCommGroup N]
[Module K N] [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N) (v : ι → M) (h : ¬LinearIndependent K v) : f v = 0 :=
by
obtain ⟨s, g, h, i, hi, hz⟩ := not_linearIndependent_iff.mp h
letI := Classical.decEq ι
suffices f (update v i (g i • v i)) = 0
by
rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this
exact Or.resolve_left this hz
rw [← Finset.insert_erase hi, Finset.sum_insert (s.notMem_erase i), add_eq_zero_iff_eq_neg] at h
rw [h, f.map_update_neg, f.map_update_sum, neg_eq_zero]
apply Finset.sum_eq_zero
intro j hj
obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj
rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]
