ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₂<GOAL>⇑e '' (⇑e ⁻¹' s) = s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₁<GOAL>⇑e ⁻¹' (⇑e '' s) = s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₁<GOAL>⇑e.symm '' (⇑e '' s) = s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₂<GOAL>⇑e '' (⇑e.symm '' s) = s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<GOAL>(ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>AddCommGroup V₃<VAR>Module k V₃<VAR>AddTorsor V₃ P₃<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>TopologicalSpace P₃<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>e' : P₂ ≃ᵃL[k] P₃<GOAL>⇑(e.trans e') = ⇑e' ∘ ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>AddCommGroup V₃<VAR>Module k V₃<VAR>AddTorsor V₃ P₃<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>TopologicalSpace P₃<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>e' : P₂ ≃ᵃL[k] P₃<VAR>p : P₁<GOAL>(e.trans e') p = e' (e p)
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>AddCommGroup V₃<VAR>Module k V₃<VAR>AddTorsor V₃ P₃<VAR>AddCommGroup V₄<VAR>Module k V₄<VAR>AddTorsor V₄ P₄<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>TopologicalSpace P₃<VAR>TopologicalSpace P₄<VAR>e₁ : P₁ ≃ᵃL[k] P₂<VAR>e₂ : P₂ ≃ᵃL[k] P₃<VAR>e₃ : P₃ ≃ᵃL[k] P₄<GOAL>(e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>e.trans (ContinuousAffineEquiv.refl k P₂) = e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>(ContinuousAffineEquiv.refl k P₁).trans e = e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>e.trans e.symm = ContinuousAffineEquiv.refl k P₁
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>e.symm.trans e = ContinuousAffineEquiv.refl k P₂
<VAR>k : Type u_1<VAR>Ring k<VAR>E : Type u_10<VAR>F : Type u_11<VAR>AddCommGroup E<VAR>Module k E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module k F<VAR>TopologicalSpace F<VAR>e : E ≃L[k] F<GOAL>⇑e.toContinuousAffineEquiv = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<VAR>ContinuousConstVAdd V₁ P₁<VAR>v : V₁<GOAL>↑(ContinuousAffineEquiv.constVAdd k P₁ v) = AffineEquiv.constVAdd k P₁ v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsRefl<VAR>x y : M<GOAL>(B x) y = 0 → (B y) x = 0
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>hB : B.IsRefl<GOAL>(-B).IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_9<VAR>CommSemiring α<VAR>Module α R<VAR>SMulCommClass R α R<VAR>NoZeroSMulDivisors α R<VAR>a : α<VAR>B : LinearMap.BilinForm R M<VAR>hB : B.IsRefl<GOAL>(a • B).IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_9<VAR>Group α<VAR>DistribMulAction α R<VAR>SMulCommClass R α R<VAR>a : α<VAR>B : LinearMap.BilinForm R M<VAR>hB : B.IsRefl<GOAL>(a • B).IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.IsRefl 0
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<GOAL>(-B).IsRefl ↔ B.IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsSymm<VAR>x y : M<GOAL>(B x) y = (B y) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsSymm<GOAL>B.IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B₁ B₂ : LinearMap.BilinForm R M<VAR>hB₁ : B₁.IsSymm<VAR>hB₂ : B₂.IsSymm<GOAL>(B₁ + B₂).IsSymm
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ B₂ : LinearMap.BilinForm R₁ M₁<VAR>hB₁ : B₁.IsSymm<VAR>hB₂ : B₂.IsSymm<GOAL>(B₁ - B₂).IsSymm
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>hB : B.IsSymm<GOAL>(-B).IsSymm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_9<VAR>Monoid α<VAR>DistribMulAction α R<VAR>SMulCommClass R α R<VAR>a : α<VAR>B : LinearMap.BilinForm R M<VAR>hB : B.IsSymm<GOAL>(a • B).IsSymm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>b : B.IsSymm<VAR>W : Submodule R M<GOAL>(B.restrict W).IsSymm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.IsSymm 0
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<GOAL>(-B).IsSymm ↔ B.IsSymm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.IsSymm ↔ LinearMap.BilinForm.flipHom B = B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsAlt<VAR>x : M<GOAL>(B x) x = 0
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>H : B₁.IsAlt<VAR>x y : M₁<GOAL>-(B₁ x) y = (B₁ y) x
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>H : B₁.IsAlt<GOAL>B₁.IsRefl
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>IsCancelAdd R<VAR>a b c : M<VAR>H : B.IsAlt<VAR>hAdd : a + b + c = 0<GOAL>(B a) b = (B b) c
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B₁ B₂ : LinearMap.BilinForm R M<VAR>hB₁ : B₁.IsAlt<VAR>hB₂ : B₂.IsAlt<GOAL>(B₁ + B₂).IsAlt
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ B₂ : LinearMap.BilinForm R₁ M₁<VAR>hB₁ : B₁.IsAlt<VAR>hB₂ : B₂.IsAlt<GOAL>(B₁ - B₂).IsAlt
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>hB : B.IsAlt<GOAL>(-B).IsAlt
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_9<VAR>Monoid α<VAR>DistribMulAction α R<VAR>SMulCommClass R α R<VAR>a : α<VAR>B : LinearMap.BilinForm R M<VAR>hB : B.IsAlt<GOAL>(a • B).IsAlt
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.IsAlt 0
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<GOAL>(-B).IsAlt ↔ B.IsAlt
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B' : LinearMap.BilinForm R M'<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>x : M<VAR>y : M'<GOAL>(B' (f x)) y = (B x) (g y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>F : LinearMap.BilinForm R M<VAR>f g : Module.End R M<GOAL>B.IsAdjointPair F f g ↔ F.compLeft f = B.compRight g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B' : LinearMap.BilinForm R M'<GOAL>B.IsAdjointPair B' 0 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.IsAdjointPair B 1 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B' : LinearMap.BilinForm R M'<VAR>f f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B.IsAdjointPair B' f' g'<GOAL>B.IsAdjointPair B' (f + f') (g + g')
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>M₁' : Type u_10<VAR>AddCommGroup M₁'<VAR>Module R₁ M₁'<VAR>B₁' : LinearMap.BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>h : B₁.IsAdjointPair B₁' f₁ g₁<VAR>h' : B₁.IsAdjointPair B₁' f₁' g₁'<GOAL>B₁.IsAdjointPair B₁' (f₁ - f₁') (g₁ - g₁')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B₂' : LinearMap.BilinForm R M'<VAR>f₂ : M →ₗ[R] M'<VAR>g₂ : M' →ₗ[R] M<VAR>c : R<VAR>h : B.IsAdjointPair B₂' f₂ g₂<GOAL>B.IsAdjointPair B₂' (c • f₂) (c • g₂)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B' : LinearMap.BilinForm R M'<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>AddCommMonoid M''<VAR>Module R M''<VAR>B'' : LinearMap.BilinForm R M''<VAR>f' : M' →ₗ[R] M''<VAR>g' : M'' →ₗ[R] M'<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B'.IsAdjointPair B'' f' g'<GOAL>B.IsAdjointPair B'' (f' ∘ₗ f) (g ∘ₗ g')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>f g f' g' : Module.End R M<VAR>h : B.IsAdjointPair B f g<VAR>h' : B.IsAdjointPair B f' g'<GOAL>B.IsAdjointPair B (f * f') (g' * g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B₂ F₂ : LinearMap.BilinForm R M<VAR>f : Module.End R M<GOAL>f ∈ B₂.isPairSelfAdjointSubmodule F₂ ↔ B₂.IsPairSelfAdjoint F₂ f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B₂ F₂ : LinearMap.BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<GOAL>B₂.IsPairSelfAdjoint F₂ f ↔ (B₂.comp ↑e ↑e).IsPairSelfAdjoint (F₂.comp ↑e ↑e) (e.symm.conj f)
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>f : Module.End R₁ M₁<GOAL>B₁.IsSkewAdjoint f ↔ (-B₁).IsAdjointPair B₁ f f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>f : Module.End R M<GOAL>f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint f
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>f : Module.End R₁ M₁<GOAL>f ∈ B₁.skewAdjointSubmodule ↔ B₁.IsSkewAdjoint f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial M<GOAL>¬LinearMap.BilinForm.Nondegenerate 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial M<VAR>B : LinearMap.BilinForm R M<VAR>h : B.Nondegenerate<GOAL>B ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B : LinearMap.BilinForm R M<VAR>e : M ≃ₗ[R] M'<VAR>h : B.Nondegenerate<GOAL>((LinearMap.BilinForm.congr e) B).Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B : LinearMap.BilinForm R M<VAR>e : M ≃ₗ[R] M'<GOAL>((LinearMap.BilinForm.congr e) B).Nondegenerate ↔ B.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.Nondegenerate ↔ LinearMap.ker B = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>h : B.Nondegenerate<GOAL>LinearMap.ker B = ⊥
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>b : B.Nondegenerate<GOAL>Function.Injective B.compLeft
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>b : B.Nondegenerate<VAR>φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁<VAR>hψ₁ : B.IsAdjointPair B ψ₁ φ<VAR>hψ₂ : B.IsAdjointPair B ψ₂ φ<GOAL>ψ₁ = ψ₂
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>b : LinearMap.SeparatingLeft B<VAR>m n : V<GOAL>((B.toDual b) m) n = (B m) n
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>f : Module.Dual K V<VAR>v : V<GOAL>(B ((B.toDual hB).symm f)) v = f v
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<GOAL>B.flip.Nondegenerate
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<GOAL>B.flip.Nondegenerate ↔ B.Nondegenerate
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_10<VAR>DecidableEq ι<VAR>Finite ι<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>b : Basis ι K V<VAR>x : V<VAR>i : ι<GOAL>((B.dualBasis hB b).repr x) i = (B x) (b i)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_10<VAR>DecidableEq ι<VAR>Finite ι<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>b : Basis ι K V<VAR>i j : ι<GOAL>(B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_10<VAR>DecidableEq ι<VAR>Finite ι<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>sym : B.IsSymm<VAR>b : Basis ι K V<VAR>i j : ι<GOAL>(B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>ι : Type u_11<VAR>Finite ι<VAR>DecidableEq ι<VAR>b : Basis ι K V<GOAL>B.dualBasis hB (B.flip.dualBasis ⋯ b) = b
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>ι : Type u_11<VAR>Finite ι<VAR>DecidableEq ι<VAR>FiniteDimensional K V<VAR>b : Basis ι K V<GOAL>B.flip.dualBasis ⋯ (B.dualBasis hB b) = b
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB' : B.IsSymm<VAR>ι : Type u_11<VAR>Finite ι<VAR>DecidableEq ι<VAR>FiniteDimensional K V<VAR>b : Basis ι K V<GOAL>B.dualBasis hB (B.dualBasis hB b) = b
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B₁ : LinearMap.BilinForm K V<VAR>B₂ : LinearMap.BilinForm K V<VAR>b₂ : B₂.Nondegenerate<VAR>v : V<GOAL>B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B₁ : LinearMap.BilinForm K V<VAR>B₂ : LinearMap.BilinForm K V<VAR>b₂ : B₂.Nondegenerate<VAR>v w : V<GOAL>(B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>b : B.Nondegenerate<VAR>φ : V →ₗ[K] V<GOAL>B.IsAdjointPair B (B.leftAdjointOfNondegenerate b φ) φ
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>b : B.Nondegenerate<VAR>ψ φ : V →ₗ[K] V<GOAL>B.IsAdjointPair B ψ φ ↔ ψ = B.leftAdjointOfNondegenerate b φ
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_4<VAR>V₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>self : P₁ ≃ᵃ[k] P₂<VAR>p : P₁<VAR>v : V₁<GOAL>self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ ≃ P₂<VAR>f' : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p<GOAL>↑{ toEquiv := f, linear := f', map_vadd' := h } = { toFun := ⇑f, linear := ↑f', map_vadd' := h }
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>(↑e).linear = ↑e.linear
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<GOAL>Function.Injective AffineEquiv.toAffineMap
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e e' : P₁ ≃ᵃ[k] P₂<GOAL>↑e = ↑e' ↔ e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>p : P₁<VAR>v : V₁<GOAL>e (v +ᵥ p) = e.linear v +ᵥ e p
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>⇑e.toEquiv = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>⇑↑e = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e e' : P₁ ≃ᵃ[k] P₂<VAR>h : ∀ (x : P₁), e x = e' x<GOAL>e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<GOAL>Function.Injective DFunLike.coe
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e e' : P₁ ≃ᵃ[k] P₂<GOAL>⇑e = ⇑e' ↔ e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<GOAL>Function.Injective AffineEquiv.toEquiv
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e e' : P₁ ≃ᵃ[k] P₂<GOAL>e.toEquiv = e'.toEquiv ↔ e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ P₂<VAR>e' : V₁ ≃ₗ[k] V₂<VAR>h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p<GOAL>⇑{ toEquiv := e, linear := e', map_vadd' := h } = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ P₂<VAR>e' : V₁ ≃ₗ[k] V₂<VAR>p : P₁<VAR>h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p<GOAL>⇑(AffineEquiv.mk' (⇑e) e' p h) = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ P₂<VAR>e' : V₁ ≃ₗ[k] V₂<VAR>p : P₁<VAR>h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p<GOAL>(AffineEquiv.mk' (⇑e) e' p h).linear = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>e.symm = e.symm.toEquiv
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>e.linear.symm = e.symm.linear
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>Function.Bijective ⇑e