ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>R₁ : Type u_10<VAR>Semiring R₁<VAR>σ : R →+* R₁<VAR>M₁ : Type u_11<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f₁ f₂ : M →ₛₗ[σ] M₁<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<GOAL>f₁ = f₂
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>R₁ : Type u_10<VAR>Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f₁ f₂ : M ≃ₛₗ[σ] M₁<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<GOAL>f₁ = f₂
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x y : M<GOAL>x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] ι →₀ R<GOAL>↑b.repr = f ↔ ∀ (i : ι), f (b i) = Finsupp.single i 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] ι →₀ R<GOAL>b.repr = f ↔ ∀ (i : ι), f (b i) = Finsupp.single i 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<VAR>i : ι<GOAL>b i = x ↔ b.repr x = Finsupp.single i 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>f : M → ι → R<VAR>hadd : ∀ (x y : M), f (x + y) = f x + f y<VAR>hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x<VAR>f_eq : ∀ (i : ι), f (b i) = ⇑(Finsupp.single i 1)<VAR>x : M<VAR>i : ι<GOAL>(b.repr x) i = f x i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b₁ b₂ : Basis ι R M<VAR>h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i<GOAL>b₁ = b₂
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b₁ b₂ : Basis ι R M<GOAL>(∀ (i : ι), b₁ i = b₂ i) → b₁ = b₂
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<GOAL>(b.map f).repr = f.symm ≪≫ₗ b.repr
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>i : ι<GOAL>(b.map f) i = f (b i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<GOAL>⇑(b.map f) = ⇑f ∘ ⇑b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>G : Type u_10<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass G R M<VAR>g : G<VAR>b : Basis ι R M<VAR>i : ι<GOAL>(g • b) i = g • b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>G : Type u_10<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass G R M<VAR>g : G<VAR>b : Basis ι R M<GOAL>⇑(g • b) = g • ⇑b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>g : M ≃ₗ[R] M<VAR>b : Basis ι R M<GOAL>g • b = b.map g
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>G : Type u_10<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass G R M<VAR>g : G<VAR>b : Basis ι R M<GOAL>(g • b).repr = (DistribMulAction.toLinearEquiv R M g).symm ≪≫ₗ b.repr
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>R' : Type u_10<VAR>Semiring R'<VAR>Module R' M<VAR>f : R ≃+* R'<VAR>h : ∀ (c : R) (x : M), f c • x = c • x<GOAL>(b.mapCoeffs f h).repr = LinearEquiv.restrictScalars R' b.repr ≪≫ₗ Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>R' : Type u_10<VAR>Semiring R'<VAR>Module R' M<VAR>f : R ≃+* R'<VAR>h : ∀ (c : R) (x : M), f c • x = c • x<VAR>i : ι<GOAL>(b.mapCoeffs f h) i = b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>R' : Type u_10<VAR>Semiring R'<VAR>Module R' M<VAR>f : R ≃+* R'<VAR>h : ∀ (c : R) (x : M), f c • x = c • x<GOAL>⇑(b.mapCoeffs f h) = ⇑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>(b.reindex e) i' = b (e.symm i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>e : ι ≃ ι'<GOAL>⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>((b.reindex e).repr x) i' = (b.repr x) (e.symm i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).repr x = Finsupp.mapDomain (⇑e) (b.repr x)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>b.reindex (Equiv.refl ι) = b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>e : ι ≃ ι'<GOAL>Set.range ⇑(b.reindex e) = Set.range ⇑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).sumCoords = b.sumCoords
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<VAR>h : b i ∈ Set.range ⇑b := ⋯<GOAL>b.reindexRange ⟨b i, h⟩ = b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>b.reindexRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : ↑(Set.range ⇑b)<GOAL>b.reindexRange x = ↑x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<VAR>bi : M<VAR>i : ι<VAR>h : b i = bi<GOAL>(b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<VAR>i : ι<VAR>h : b i ∈ Set.range ⇑b := ⋯<GOAL>(b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Fintype ι<VAR>DecidableEq M<VAR>i : ι<VAR>h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯<GOAL>b.reindexFinsetRange ⟨b i, h⟩ = b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Fintype ι<VAR>DecidableEq M<VAR>x : { x // x ∈ Finset.image (⇑b) Finset.univ }<GOAL>b.reindexFinsetRange x = ↑x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Fintype ι<VAR>DecidableEq M<VAR>i : ι<GOAL>b.reindexFinsetRange.repr (b i) = Finsupp.single ⟨b i, ⋯⟩ 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Fintype ι<VAR>DecidableEq M<VAR>x : M<VAR>i : ι<VAR>h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯<GOAL>(b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>LinearIndependent R ⇑b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Nontrivial R<VAR>i : ι<GOAL>b i ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<GOAL>x ∈ Submodule.span R (Set.range ⇑b)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>Submodule.span R (Set.range ⇑b) = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Nontrivial M<GOAL>Nonempty ι
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Submodule R M<VAR>b : Basis ι R ↥P<VAR>x : M<GOAL>x ∈ P ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : ι → M'<GOAL>(b.constr S) f = Finsupp.total M' M' R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : ι → M'<VAR>x : M<GOAL>((b.constr S) f) x = (b.repr x).sum fun b a => a • f b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : ι → M'<VAR>i : ι<GOAL>((b.constr S) f) (b i) = f i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>g : ι → M'<VAR>f : M →ₗ[R] M'<VAR>h : ∀ (i : ι), g i = f (b i)<GOAL>(b.constr S) g = f
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : M →ₗ[R] M'<GOAL>((b.constr S) fun i => f (b i)) = f
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : ι → M'<GOAL>LinearMap.range ((b.constr S) f) = Submodule.span R (Set.range f)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>f : M' →ₗ[R] M'<VAR>v : ι → M'<GOAL>(b.constr S) (⇑f ∘ v) = f ∘ₗ (b.constr S) v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>i : ι<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<GOAL>(b.equiv b' e) (b i) = b' (e i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<GOAL>(b.equiv b' e).symm = b'.equiv b e.symm
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>AddCommMonoid M''<VAR>Module R M''<VAR>ι'' : Type u_10<VAR>b'' : Basis ι'' R M''<VAR>e : ι ≃ ι'<VAR>e' : ι' ≃ ι''<GOAL>b.equiv b' e ≪≫ₗ b'.equiv b'' e' = b.equiv b'' (e.trans e')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<GOAL>b.map (b.equiv b' e) = b'.reindex e.symm
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>x : M × M'<VAR>i : ι<GOAL>((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>x : M × M'<VAR>i : ι'<GOAL>((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>i : ι<GOAL>((b.prod b') (Sum.inl i)).1 = b i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>i : ι'<GOAL>((b.prod b') (Sum.inr i)).1 = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>i : ι<GOAL>((b.prod b') (Sum.inl i)).2 = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>i : ι'<GOAL>((b.prod b') (Sum.inr i)).2 = b' i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>i : ι ⊕ ι'<GOAL>(b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroDivisors R<VAR>b : Basis ι R M<GOAL>NoZeroSMulDivisors R M
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroDivisors R<VAR>b : Basis ι R M<VAR>c : R<VAR>x : M<GOAL>c • x = 0 ↔ c = 0 ∨ x = 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0<GOAL>N = ⊥
<VAR>ι : Type u_10<VAR>R : Type u_11<VAR>Unique ι<VAR>Semiring R<VAR>i : ι<GOAL>(Basis.singleton ι R) i = 1
<VAR>ι : Type u_10<VAR>R : Type u_11<VAR>Unique ι<VAR>Semiring R<VAR>x : R<VAR>i : ι<GOAL>((Basis.singleton ι R).repr x) i = x
<VAR>R : Type u_10<VAR>M : Type u_11<VAR>Ring R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>ι : Type u_12<VAR>Unique ι<GOAL>Nonempty (Basis ι R M) ↔ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>Fintype R<VAR>Fintype M<GOAL>Fintype.card M = Fintype.card R ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>x : ι → R<GOAL>b.equivFun.symm x = ∑ i : ι, x i • b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>b : Basis ι R M<VAR>u : M<GOAL>b.equivFun u = ⇑(b.repr u)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>Finite ι<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<GOAL>(b.map f).equivFun = f.symm ≪≫ₗ b.equivFun
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>u : M<GOAL>∑ i : ι, b.equivFun u i • b i = u
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>u : M<GOAL>∑ i : ι, (b.repr u) i • b i = u
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>i j : ι<GOAL>b.equivFun (b i) j = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>c : ι → R<GOAL>⇑(b.repr (∑ i : ι, c i • b i)) = c
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>e : M ≃ₗ[R] ι → R<VAR>x : M<VAR>i : ι<GOAL>((Basis.ofEquivFun e).repr x) i = e x i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>DecidableEq ι<VAR>e : M ≃ₗ[R] ι → R<GOAL>⇑(Basis.ofEquivFun e) = fun i => e.symm (Function.update 0 i 1)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>v : Basis ι R M<GOAL>Basis.ofEquivFun v.equivFun = v
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>e : M ≃ₗ[R] ι → R<GOAL>(Basis.ofEquivFun e).equivFun = e
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>S : Type u_10<VAR>Semiring S<VAR>Module S M'<VAR>SMulCommClass R S M'<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : ι → M'<VAR>x : M<GOAL>((b.constr S) f) x = ∑ i : ι, b.equivFun x i • f i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>P : Submodule R M<VAR>b : Basis ι R ↥P<VAR>x : M<GOAL>x ∈ P ↔ ∃ c, x = ∑ i : ι, c i • ↑(b i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>b : Basis ι R M<VAR>i : ι<VAR>f : ι → R<GOAL>(b.coord i) (b.equivFun.symm f) = f i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>f : M → M'<VAR>g : M' → M<VAR>hf : ∀ (i : ι), f (b i) ∈ Set.range ⇑b'<VAR>hg : ∀ (i : ι'), g (b' i) ∈ Set.range ⇑b<VAR>hgf : ∀ (i : ι), g (f (b i)) = b i<VAR>hfg : ∀ (i : ι'), f (g (b' i)) = b' i<VAR>i : ι<GOAL>(b.equiv' b' f g hf hg hgf hfg) (b i) = f (b i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M'<VAR>f : M → M'<VAR>g : M' → M<VAR>hf : ∀ (i : ι), f (b i) ∈ Set.range ⇑b'<VAR>hg : ∀ (i : ι'), g (b' i) ∈ Set.range ⇑b<VAR>hgf : ∀ (i : ι), g (f (b i)) = b i<VAR>hfg : ∀ (i : ι'), f (g (b' i)) = b' i<VAR>i : ι'<GOAL>(b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>ι' : Type u_10<VAR>Fintype ι'<VAR>b' : Basis ι' R M<VAR>x : M<VAR>i : ι<GOAL>∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>b : Basis ι R M<GOAL>⋯.Maximal
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<GOAL>(Basis.mk hli hsp).repr x = hli.repr ⟨x, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<VAR>i : ι<GOAL>(Basis.mk hli hsp) i = v i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<GOAL>⇑(Basis.mk hli hsp) = v
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<VAR>i : ι<GOAL>((Basis.mk hli hsp).coord i) (v i) = 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<VAR>i j : ι<VAR>h : j ≠ i<GOAL>((Basis.mk hli hsp).coord i) (v j) = 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<VAR>DecidableEq ι<VAR>i j : ι<GOAL>((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hli : LinearIndependent R v<VAR>i : ι<GOAL>↑((Basis.span hli) i) = v i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>G : Type u_10<VAR>Group G<VAR>DistribMulAction G R<VAR>DistribMulAction G M<VAR>IsScalarTower G R M<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>w : ι → G<GOAL>Submodule.span R (Set.range (w • v)) = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>G : Type u_10<VAR>Group G<VAR>DistribMulAction G R<VAR>DistribMulAction G M<VAR>IsScalarTower G R M<VAR>SMulCommClass G R M<VAR>v : Basis ι R M<VAR>w : ι → G<VAR>i : ι<GOAL>(v.groupSMul w) i = (w • ⇑v) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>w : ι → Rˣ<GOAL>Submodule.span R (Set.range (w • v)) = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v : Basis ι R M<VAR>w : ι → Rˣ<VAR>i : ι<GOAL>(v.unitsSMul w) i = w i • v i
<VAR>ι : Type u_1<VAR>R₂ : Type u_4<VAR>M : Type u_6<VAR>CommRing R₂<VAR>AddCommGroup M<VAR>Module R₂ M<VAR>e : Basis ι R₂ M<VAR>w : ι → R₂ˣ<VAR>i : ι<GOAL>(e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
<VAR>ι : Type u_1<VAR>R₂ : Type u_4<VAR>M : Type u_6<VAR>CommRing R₂<VAR>AddCommGroup M<VAR>Module R₂ M<VAR>e : Basis ι R₂ M<VAR>w : ι → R₂ˣ<VAR>v : M<VAR>i : ι<GOAL>((e.unitsSMul w).repr v) i = (w i)⁻¹ • (e.repr v) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v : Basis ι R M<VAR>w : ι → R<VAR>hw : ∀ (i : ι), IsUnit (w i)<VAR>i : ι<GOAL>(v.isUnitSMul hw) i = w i • v i
<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>y : M<VAR>b : Basis (Fin n) R ↥N<VAR>hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0<VAR>hsp : ∀ (z : M), ∃ c, z + c • y ∈ N<GOAL>⇑(Basis.mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)