ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<GOAL>s • ⊥ = ⊥
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>N : Submodule R M<VAR>SMulCommClass S R M<VAR>r : S<GOAL>{r} • N = r • N
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>N : Submodule R M<VAR>SMulCommClass R S M<VAR>r : S<VAR>x : M<GOAL>x ∈ {r} • N ↔ ∃ m ∈ N, x = r • m
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>N : Submodule R M<VAR>s t : Set S<GOAL>(s ⊔ t) • N = s • N ⊔ t • N
<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>CommSemiring R'<VAR>AddCommMonoid M'<VAR>Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<GOAL>↑(Ideal.span s) • N = s • N
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<GOAL>MvPolynomial.supported R s = (MvPolynomial.rename Subtype.val).range
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<VAR>x : R<GOAL>(MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.C x) = (algebraMap R ↥(MvPolynomial.supported R s)) x
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<VAR>i : ↑s<GOAL>↑((MvPolynomial.supportedEquivMvPolynomial s).symm (MvPolynomial.X i)) = MvPolynomial.X ↑i
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>s : Set σ<GOAL>p ∈ MvPolynomial.supported R s ↔ ↑p.vars ⊆ s
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<GOAL>↑(MvPolynomial.supported R s) = {p | ↑p.vars ⊆ s}
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p ∈ MvPolynomial.supported R ↑p.vars
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<GOAL>MvPolynomial.supported R s = Algebra.adjoin R (MvPolynomial.X '' s)
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<GOAL>MvPolynomial.supported R Set.univ = ⊤
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<GOAL>MvPolynomial.supported R ∅ = ⊥
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set σ<VAR>st : s ⊆ t<GOAL>MvPolynomial.supported R s ≤ MvPolynomial.supported R t
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set σ<VAR>Nontrivial R<VAR>i : σ<GOAL>MvPolynomial.X i ∈ MvPolynomial.supported R s ↔ i ∈ s
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>s t : Set σ<VAR>Nontrivial R<GOAL>MvPolynomial.supported R s ≤ MvPolynomial.supported R t ↔ s ⊆ t
<VAR>σ : Type u_1<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>StrictMono (MvPolynomial.supported R)
<VAR>σ : Type u_1<VAR>s : Set σ<VAR>R : Type u_3<VAR>CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>hF : ↑F.vars ⊆ s<GOAL>∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (MvPolynomial.aeval x) F
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>i : σ<GOAL>MvPolynomial.pderiv i = MvPolynomial.mkDerivation R (Pi.single i 1)
<VAR>R : Type u<VAR>σ : Type v<VAR>a : R<VAR>s : σ →₀ ℕ<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial (s - Finsupp.single i 1)) (a * ↑(s i))
<VAR>R : Type u<VAR>σ : Type v<VAR>a : R<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) (MvPolynomial.C a) = 0
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) 1 = 0
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>i j : σ<GOAL>(MvPolynomial.pderiv i) (MvPolynomial.X j) = Pi.single i 1 j
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) (MvPolynomial.X i) = 1
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i j : σ<VAR>h : j ≠ i<GOAL>(MvPolynomial.pderiv i) (MvPolynomial.X j) = 0
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i : σ<VAR>f : MvPolynomial σ R<VAR>h : i ∉ f.vars<GOAL>(MvPolynomial.pderiv i) f = 0
<VAR>R : Type u<VAR>σ : Type v<VAR>a : R<VAR>CommSemiring R<VAR>i : σ<VAR>n : ℕ<GOAL>(MvPolynomial.pderiv i) ((MvPolynomial.monomial (Finsupp.single i n)) a) = (MvPolynomial.monomial (Finsupp.single i (n - 1))) (a * ↑n)
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i : σ<VAR>f g : MvPolynomial σ R<GOAL>(MvPolynomial.pderiv i) (f * g) = (MvPolynomial.pderiv i) f * g + f * (MvPolynomial.pderiv i) g
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>i : σ<VAR>f : MvPolynomial σ R<VAR>n : ℕ<GOAL>(MvPolynomial.pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (MvPolynomial.pderiv i) f
<VAR>R : Type u<VAR>σ : Type v<VAR>a : R<VAR>CommSemiring R<VAR>f : MvPolynomial σ R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) (MvPolynomial.C a * f) = MvPolynomial.C a * (MvPolynomial.pderiv i) f
<VAR>R : Type u<VAR>σ : Type v<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>φ : R →+* S<VAR>f : MvPolynomial σ R<VAR>i : σ<GOAL>(MvPolynomial.pderiv i) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((MvPolynomial.pderiv i) f)
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>f : M ≃ₗ[S] M₂<VAR>a : M<GOAL>(LinearEquiv.restrictScalars R f) a = f a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>f : M ≃ₗ[S] M₂<VAR>a : M₂<GOAL>(LinearEquiv.restrictScalars R f).symm a = f.symm a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<GOAL>Function.Injective (LinearEquiv.restrictScalars R)
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>f g : M ≃ₗ[S] M₂<GOAL>LinearEquiv.restrictScalars R f = LinearEquiv.restrictScalars R g ↔ f = g
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<GOAL>IsUnit f ↔ Function.Bijective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑1 = id
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑1 = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e₁ e₂ : M ≃ₗ[R] M<GOAL>↑(e₁ * e₂) = ↑e₁ * ↑e₂
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃ₗ[R] M<VAR>n : ℕ<GOAL>⇑(e ^ n) = (⇑e)^[n]
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃ₗ[R] M<VAR>n : ℕ<VAR>m : M<GOAL>(e ^ n) m = (⇑e)^[n] m
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃ₗ[R] M<GOAL>LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = ↑e
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M ≃ₗ[R] M<VAR>a : M<GOAL>f • a = f a
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Subsingleton M<VAR>Subsingleton M₂<GOAL>∀ (x : M₂), (LinearEquiv.ofSubsingleton M M₂).symm x = 0
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Subsingleton M<VAR>Subsingleton M₂<GOAL>∀ (x : M), (LinearEquiv.ofSubsingleton M M₂) x = 0
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton M<GOAL>LinearEquiv.ofSubsingleton M M = LinearEquiv.refl R M
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring R<VAR>Semiring S<VAR>g : R ≃+* S<VAR>a : R<GOAL>(Module.compHom.toLinearEquiv g) a = g a
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring R<VAR>Semiring S<VAR>g : R ≃+* S<VAR>a : S<GOAL>(Module.compHom.toLinearEquiv g).symm a = g.symm a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Group S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>∀ (a : M), (DistribMulAction.toLinearEquiv R M s).symm a = s⁻¹ • a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Group S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>∀ (a : M), (DistribMulAction.toLinearEquiv R M s) a = s • a
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Group S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<GOAL>(DistribMulAction.toModuleAut R M) s = DistribMulAction.toLinearEquiv R M s
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃+ M₂<VAR>h : ∀ (c : R) (x : M), e (c • x) = c • e x<GOAL>⇑(e.toLinearEquiv h) = ⇑e
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃+ M₂<VAR>h : ∀ (c : R) (x : M), e (c • x) = c • e x<GOAL>⇑(e.toLinearEquiv h).symm = ⇑e.symm
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>e : M ≃+ M₂<GOAL>⇑e.toNatLinearEquiv = ⇑e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>e : M ≃+ M₂<GOAL>↑e.toNatLinearEquiv = e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>e : M ≃ₗ[ℕ] M₂<GOAL>(↑e).toNatLinearEquiv = e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>e : M ≃+ M₂<GOAL>e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv
<VAR>M : Type u_8<VAR>AddCommMonoid M<GOAL>(AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>e : M ≃+ M₂<VAR>e₂ : M₂ ≃+ M₃<GOAL>e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>e : M ≃+ M₂<GOAL>⇑e.toIntLinearEquiv = ⇑e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>e : M ≃+ M₂<GOAL>↑e.toIntLinearEquiv = e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>e : M ≃ₗ[ℤ] M₂<GOAL>(↑e).toIntLinearEquiv = e
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>e : M ≃+ M₂<GOAL>e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv
<VAR>M : Type u_8<VAR>AddCommGroup M<GOAL>(AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M
<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>e : M ≃+ M₂<VAR>e₂ : M₂ ≃+ M₃<GOAL>e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : R →ₗ[R] M<GOAL>(LinearMap.ringLmapEquivSelf R S M) f = f 1
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>x : M<GOAL>(LinearMap.ringLmapEquivSelf R S M).symm x = LinearMap.smulRight 1 x
<VAR>A : Type u_17<VAR>B : Type u_18<VAR>R : Type u_19<VAR>Semiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R B<VAR>f : A →+ B<GOAL>(addMonoidHomLequivNat R) f = f.toNatLinearMap
<VAR>A : Type u_17<VAR>B : Type u_18<VAR>R : Type u_19<VAR>Semiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R B<VAR>f : A →ₗ[ℕ] B<GOAL>(addMonoidHomLequivNat R).symm f = f.toAddMonoidHom
<VAR>A : Type u_17<VAR>B : Type u_18<VAR>R : Type u_19<VAR>Semiring R<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>Module R B<VAR>f : A →ₗ[ℤ] B<GOAL>(addMonoidHomLequivInt R).symm f = f.toAddMonoidHom
<VAR>A : Type u_17<VAR>B : Type u_18<VAR>R : Type u_19<VAR>Semiring R<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>Module R B<VAR>f : A →+ B<GOAL>(addMonoidHomLequivInt R) f = f.toIntLinearMap
<VAR>A : Type u_17<VAR>AddCommGroup A<GOAL>∀ (a : A →+ A), (addMonoidEndRingEquivInt A) a = (↑(addMonoidHomLequivInt ℤ)).toFun a
<VAR>A : Type u_17<VAR>AddCommGroup A<GOAL>∀ (a : A →ₗ[ℤ] A), (addMonoidEndRingEquivInt A).symm a = (addMonoidHomLequivInt ℤ).invFun a
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>Subsingleton M<VAR>Subsingleton M₂<GOAL>LinearEquiv.symm 0 = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>Subsingleton M<VAR>Subsingleton M₂<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>Subsingleton M<VAR>Subsingleton M₂<VAR>x : M<GOAL>0 x = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>V : Type u_18<VAR>V₂ : Type u_17<GOAL>⇑(LinearEquiv.curry R V V₂) = Function.curry
<VAR>R : Type u_1<VAR>Semiring R<VAR>V : Type u_18<VAR>V₂ : Type u_17<GOAL>⇑(LinearEquiv.curry R V V₂).symm = Function.uncurry
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f = LinearMap.id<VAR>x : M<GOAL>(LinearEquiv.ofLinear f g h₁ h₂) x = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f = LinearMap.id<VAR>x : M₂<GOAL>(LinearEquiv.ofLinear f g h₁ h₂).symm x = g x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f = LinearMap.id<GOAL>↑(LinearEquiv.ofLinear f g h₁ h₂) = f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f = LinearMap.id<GOAL>↑(LinearEquiv.ofLinear f g h₁ h₂).symm = g
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>⇑(LinearEquiv.neg R) = -id
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<GOAL>(LinearEquiv.neg R) x = -x
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>(LinearEquiv.neg R).symm = LinearEquiv.neg R
<VAR>R : Type u_17<VAR>M₁ : Type u_18<VAR>M₂ : Type u_19<VAR>M₂₁ : Type u_20<VAR>M₂₂ : Type u_21<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₂₁<VAR>AddCommMonoid M₂₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₂₁<VAR>Module R M₂₂<VAR>e₁ : M₁ ≃ₗ[R] M₂<VAR>e₂ : M₂₁ ≃ₗ[R] M₂₂<VAR>f : M₁ →ₗ[R] M₂₁<VAR>x : M₂<GOAL>((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
<VAR>R : Type u_17<VAR>M₁ : Type u_18<VAR>M₂ : Type u_19<VAR>M₂₁ : Type u_20<VAR>M₂₂ : Type u_21<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₂₁<VAR>AddCommMonoid M₂₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₂₁<VAR>Module R M₂₂<VAR>e₁ : M₁ ≃ₗ[R] M₂<VAR>e₂ : M₂₁ ≃ₗ[R] M₂₂<VAR>f : M₂ →ₗ[R] M₂₂<VAR>x : M₁<GOAL>((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>N : Type u_17<VAR>N₂ : Type u_18<VAR>N₃ : Type u_19<VAR>AddCommMonoid N<VAR>AddCommMonoid N₂<VAR>AddCommMonoid N₃<VAR>Module R N<VAR>Module R N₂<VAR>Module R N₃<VAR>e₁ : M ≃ₗ[R] N<VAR>e₂ : M₂ ≃ₗ[R] N₂<VAR>e₃ : M₃ ≃ₗ[R] N₃<VAR>f : M →ₗ[R] M₂<VAR>g : M₂ →ₗ[R] M₃<GOAL>(e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_17<VAR>M₂ : Type u_18<VAR>M₃ : Type u_19<VAR>N₁ : Type u_20<VAR>N₂ : Type u_21<VAR>N₃ : Type u_22<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>AddCommMonoid N₁<VAR>Module R N₁<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>AddCommMonoid N₃<VAR>Module R N₃<VAR>e₁ : M₁ ≃ₗ[R] M₂<VAR>e₂ : N₁ ≃ₗ[R] N₂<VAR>e₃ : M₂ ≃ₗ[R] M₃<VAR>e₄ : N₂ ≃ₗ[R] N₃<GOAL>e₁.arrowCongr e₂ ≪≫ₗ e₃.arrowCongr e₄ = (e₁ ≪≫ₗ e₃).arrowCongr (e₂ ≪≫ₗ e₄)
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>f : Module.End R M<GOAL>e.conj f = (↑e ∘ₗ f) ∘ₗ ↑e.symm
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>f : Module.End R M<VAR>x : M₂<GOAL>(e.conj f) x = e (f (e.symm x))
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>f : Module.End R M₂<GOAL>e.symm.conj f = (↑e.symm ∘ₗ f) ∘ₗ ↑e
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>f g : Module.End R M<GOAL>e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>e₁ : M ≃ₗ[R] M₂<VAR>e₂ : M₂ ≃ₗ[R] M₃<GOAL>e₁.conj ≪≫ₗ e₂.conj = (e₁ ≪≫ₗ e₂).conj
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<GOAL>e.conj LinearMap.id = LinearMap.id
<VAR>K : Type u_6<VAR>M : Type u_8<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>a : K<VAR>ha : a ≠ 0<GOAL>∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha).symm a_1 = (Units.mk0 a ha)⁻¹ • a_1
<VAR>K : Type u_6<VAR>M : Type u_8<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>a : K<VAR>ha : a ≠ 0<GOAL>∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = Units.mk0 a ha • a_1
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>f : m → n<VAR>g : n → M<VAR>i : m<GOAL>(LinearMap.funLeft R M f) g i = g (f i)
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : Type u_18<VAR>g : n → M<GOAL>(LinearMap.funLeft R M id) g = g
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>f₁ : n → p<VAR>f₂ : m → n<GOAL>LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>f : m → n<VAR>hf : Function.Injective f<GOAL>Function.Surjective ⇑(LinearMap.funLeft R M f)
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>f : m → n<VAR>hf : Function.Surjective f<GOAL>Function.Injective ⇑(LinearMap.funLeft R M f)
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>e : m ≃ n<VAR>x : n → M<GOAL>(LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : Type u_18<GOAL>LinearEquiv.funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>p : Type u_19<VAR>e₁ : m ≃ n<VAR>e₂ : n ≃ p<GOAL>LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : Type u_17<VAR>n : Type u_18<VAR>e : m ≃ n<GOAL>(LinearEquiv.funCongrLeft R M e).symm = LinearEquiv.funCongrLeft R M e.symm
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>↑(Submodule.map f p) = ⇑f '' ↑p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<GOAL>(Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (↑f) p.toAddSubmonoid
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<GOAL>(Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid
<VAR>A : Type u_10<VAR>A₂ : Type u_11<VAR>AddCommGroup A<VAR>AddCommGroup A₂<VAR>f : A →+ A₂<VAR>s : AddSubgroup A<GOAL>Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
<VAR>G : Type u_10<VAR>G₂ : Type u_11<VAR>Group G<VAR>Group G₂<VAR>f : G →* G₂<VAR>s : Subgroup G<GOAL>AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
<VAR>G : Type u_10<VAR>G₂ : Type u_11<VAR>AddGroup G<VAR>AddGroup G₂<VAR>f : G →+ G₂<VAR>s : AddSubgroup G<GOAL>Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.map f s)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>x : M₂<GOAL>x ∈ Submodule.map f p ↔ ∃ y ∈ p, f y = x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>r : M<VAR>h : r ∈ p<GOAL>f r ∈ Submodule.map f p