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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>Function.Surjective ⇑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>Function.Injective ⇑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>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Bijective ⇑φ<GOAL>(AffineEquiv.ofBijective hφ).linear = LinearEquiv.ofBijective φ.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>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Bijective ⇑φ<VAR>a : P₁<GOAL>(AffineEquiv.ofBijective hφ) a = φ a
<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>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Bijective ⇑φ<GOAL>(AffineEquiv.ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ) hφ).symm
<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>Set.range ⇑e = Set.univ
<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₂<GOAL>e (e.symm p) = 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₂<VAR>p : P₁<GOAL>e.symm (e p) = 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₂<VAR>p₁ : P₁<VAR>p₂ : P₂<GOAL>e p₁ = p₂ ↔ p₁ = e.symm 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₂<VAR>p₁ p₂ : P₁<GOAL>e p₁ = e p₂ ↔ p₁ = 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₁ ≃ᵃ[k] P₂<VAR>s : Set P₂<GOAL>⇑f.symm '' s = ⇑f ⁻¹' 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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ ≃ᵃ[k] P₂<VAR>s : Set P₁<GOAL>⇑f.symm ⁻¹' s = ⇑f '' 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>AffineSpace V₁ P₁<GOAL>⇑(AffineEquiv.refl k P₁) = id
<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>AffineSpace V₁ P₁<GOAL>↑(AffineEquiv.refl k P₁) = AffineMap.id k P₁
<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>AffineSpace V₁ P₁<VAR>x : P₁<GOAL>(AffineEquiv.refl k P₁) x = x
<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>AffineSpace V₁ P₁<GOAL>(AffineEquiv.refl k P₁).toEquiv = Equiv.refl P₁
<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>AffineSpace V₁ P₁<GOAL>(AffineEquiv.refl k P₁).linear = LinearEquiv.refl k V₁
<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>AffineSpace V₁ P₁<GOAL>(AffineEquiv.refl k P₁).symm = AffineEquiv.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>AffineSpace V₁ P₁<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>e' : P₂ ≃ᵃ[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>AffineSpace V₁ P₁<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>e' : P₂ ≃ᵃ[k] P₃<GOAL>↑(e.trans e') = (↑e').comp ↑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>AffineSpace V₁ P₁<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>e' : P₂ ≃ᵃ[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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<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>e₂ : P₂ ≃ᵃ[k] P₃<VAR>e₃ : P₃ ≃ᵃ[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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>e.trans (AffineEquiv.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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>(AffineEquiv.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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>e.trans e.symm = AffineEquiv.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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>e.symm.trans e = AffineEquiv.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>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>a b : P₁<VAR>c : k<GOAL>e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c
<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>AffineSpace V₁ P₁<GOAL>1 = AffineEquiv.refl k P₁
<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>AffineSpace V₁ P₁<GOAL>⇑1 = id
<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>AffineSpace V₁ P₁<VAR>e e' : P₁ ≃ᵃ[k] P₁<GOAL>e * e' = e'.trans 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>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>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>e : P₁ ≃ᵃ[k] P₁<GOAL>e⁻¹ = e.symm
<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>AffineSpace V₁ P₁<VAR>self : P₁ ≃ᵃ[k] P₁<GOAL>AffineEquiv.linearHom self = self.linear
<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>AffineSpace V₁ P₁<VAR>u : (P₁ →ᵃ[k] P₁)ˣ<GOAL>(AffineEquiv.equivUnitsAffineMap.symm u).linear = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)
<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>AffineSpace V₁ P₁<VAR>u : (P₁ →ᵃ[k] P₁)ˣ<VAR>a : P₁<GOAL>(AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a
<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>AffineSpace V₁ P₁<VAR>e : P₁ ≃ᵃ[k] P₁<GOAL>↑(AffineEquiv.equivUnitsAffineMap e) = ↑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>AffineSpace V₁ P₁<VAR>e : P₁ ≃ᵃ[k] P₁<GOAL>↑(AffineEquiv.equivUnitsAffineMap e)⁻¹ = ↑e.symm
<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>AffineSpace V₁ P₁<VAR>u : (P₁ →ᵃ[k] P₁)ˣ<VAR>a : P₁<GOAL>(AffineEquiv.equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a
<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>AffineSpace V₁ P₁<VAR>u : (P₁ →ᵃ[k] P₁)ˣ<VAR>a : P₁<GOAL>(AffineEquiv.equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a
<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>AffineSpace V₁ P₁<VAR>b : P₁<GOAL>(AffineEquiv.vaddConst k b).linear = LinearEquiv.refl k V₁
<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>AffineSpace V₁ P₁<VAR>b p' : P₁<GOAL>(AffineEquiv.vaddConst k b).symm p' = p' -ᵥ b
<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>AffineSpace V₁ P₁<VAR>b : P₁<VAR>v : V₁<GOAL>(AffineEquiv.vaddConst k b) v = v +ᵥ b
<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>AffineSpace V₁ P₁<VAR>p : P₁<GOAL>⇑(AffineEquiv.constVSub k p) = fun x => p -ᵥ x
<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>AffineSpace V₁ P₁<VAR>p : P₁<GOAL>⇑(AffineEquiv.constVSub k p).symm = fun v => -v +ᵥ p
<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>AffineSpace V₁ P₁<VAR>v : V₁<GOAL>(AffineEquiv.constVAdd k P₁ v).linear = LinearEquiv.refl k V₁
<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>AffineSpace V₁ P₁<VAR>v : V₁<GOAL>∀ (x : P₁), (AffineEquiv.constVAdd k P₁ v) x = v +ᵥ x
<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>AffineSpace V₁ P₁<GOAL>AffineEquiv.constVAdd k P₁ 0 = AffineEquiv.refl k P₁
<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>AffineSpace V₁ P₁<VAR>v w : V₁<GOAL>AffineEquiv.constVAdd k P₁ (v + w) = (AffineEquiv.constVAdd k P₁ w).trans (AffineEquiv.constVAdd k P₁ v)
<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>AffineSpace V₁ P₁<VAR>v : V₁<GOAL>(AffineEquiv.constVAdd k P₁ v).symm = AffineEquiv.constVAdd k P₁ (-v)
<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>AffineSpace V₁ P₁<VAR>v : Multiplicative V₁<GOAL>(AffineEquiv.constVAddHom k P₁) v = AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v)
<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>AffineSpace V₁ P₁<VAR>n : ℕ<VAR>v : V₁<GOAL>AffineEquiv.constVAdd k P₁ (n • v) = AffineEquiv.constVAdd k P₁ v ^ n
<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>AffineSpace V₁ P₁<VAR>z : ℤ<VAR>v : V₁<GOAL>AffineEquiv.constVAdd k P₁ (z • v) = AffineEquiv.constVAdd k P₁ v ^ z
<VAR>R : Type u_10<VAR>V : Type u_11<VAR>P : Type u_12<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AffineSpace V P<VAR>p : P<VAR>t : Rˣ<GOAL>⇑((AffineEquiv.homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)
<VAR>R : Type u_10<VAR>V : Type u_11<VAR>P : Type u_12<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AffineSpace V P<VAR>p : P<VAR>t : Rˣ<GOAL>⇑((AffineEquiv.homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)
<VAR>R : Type u_10<VAR>V : Type u_11<VAR>P : Type u_12<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AffineSpace V P<VAR>p : P<GOAL>AffineEquiv.toAffineMap ∘ ⇑(AffineEquiv.homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val
<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>AffineSpace V₁ P₁<VAR>x y : P₁<GOAL>(AffineEquiv.pointReflection k x) y = x -ᵥ y +ᵥ x
<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>AffineSpace V₁ P₁<VAR>x : P₁<GOAL>(AffineEquiv.pointReflection k x).symm = AffineEquiv.pointReflection k x
<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>AffineSpace V₁ P₁<VAR>x : P₁<GOAL>(AffineEquiv.pointReflection k x).toEquiv = Equiv.pointReflection x
<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>AffineSpace V₁ P₁<VAR>x : P₁<GOAL>(AffineEquiv.pointReflection k x) x = x
<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>AffineSpace V₁ P₁<VAR>x : P₁<GOAL>Function.Involutive ⇑(AffineEquiv.pointReflection k x)
<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>AffineSpace V₁ P₁<VAR>x y : P₁<VAR>h : Function.Injective fun x => 2 • x<GOAL>(AffineEquiv.pointReflection k x) y = y ↔ y = x
<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>AffineSpace V₁ P₁<VAR>h : Function.Injective fun x => 2 • x<VAR>y : P₁<GOAL>Function.Injective fun x => (AffineEquiv.pointReflection k x) y
<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>AffineSpace V₁ P₁<VAR>Invertible 2<VAR>y : P₁<GOAL>Function.Injective fun x => (AffineEquiv.pointReflection k x) y
<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>AffineSpace V₁ P₁<VAR>Invertible 2<VAR>x y : P₁<GOAL>(AffineEquiv.pointReflection k x) y = y ↔ y = x
<VAR>k : Type u_1<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>e : V₁ ≃ₗ[k] V₂<GOAL>⇑e.toAffineEquiv = ⇑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>AffineSpace V₁ P₁<VAR>v v' : V₁<VAR>p : P₁<VAR>c : k<GOAL>(AffineMap.lineMap v v') c +ᵥ p = (AffineMap.lineMap (v +ᵥ p) (v' +ᵥ p)) c
<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>AffineSpace V₁ P₁<VAR>p₁ p₂ p₃ : P₁<VAR>c : k<GOAL>(AffineMap.lineMap p₁ p₂) c -ᵥ p₃ = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c
<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>AffineSpace V₁ P₁<VAR>p₁ p₂ p₃ : P₁<VAR>c : k<GOAL>p₁ -ᵥ (AffineMap.lineMap p₂ p₃) c = (AffineMap.lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c
<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>AffineSpace V₁ P₁<VAR>v : V₁<VAR>p₁ p₂ : P₁<VAR>c : k<GOAL>v +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v +ᵥ p₁) (v +ᵥ p₂)) c
<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>AddCommGroup V₁<VAR>AffineSpace V₁ P₁<VAR>R' : Type u_10<VAR>CommRing R'<VAR>Module R' V₁<VAR>c p : P₁<GOAL>(AffineMap.homothety c (-1)) p = (AffineEquiv.pointReflection R' c) p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ιι : Type u_3<VAR>ι : ιι → Type u_4<VAR>a b : GradedMonoid fun ii => ⨂[R] (x : ι ii), M<VAR>h : a.fst = b.fst<GOAL>(PiTensorProduct.reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd → a = b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>GradedMonoid.GOne.one = (PiTensorProduct.tprod R) Fin.elim0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>GradedMonoid.GMul.mul a b = TensorPower.mulEquiv (a ⊗ₜ[R] b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>GradedMonoid.GMul.mul a b = (((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑TensorPower.mulEquiv) a) b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>h : i = j<VAR>a : Fin i → M<GOAL>(TensorPower.cast R M h) ((PiTensorProduct.tprod R) a) = (PiTensorProduct.tprod R) (a ∘ Fin.cast ⋯)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i : ℕ<VAR>h : i = i<GOAL>TensorPower.cast R M h = LinearEquiv.refl R (⨂[R]^i M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>h : i = j<GOAL>(TensorPower.cast R M h).symm = TensorPower.cast R M ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j k : ℕ<VAR>h : i = j<VAR>h' : j = k<GOAL>TensorPower.cast R M h ≪≫ₗ TensorPower.cast R M h' = TensorPower.cast R M ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j k : ℕ<VAR>h : i = j<VAR>h' : j = k<VAR>a : ⨂[R]^i M<GOAL>(TensorPower.cast R M h') ((TensorPower.cast R M h) a) = (TensorPower.cast R M ⋯) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M<VAR>h : a.fst = b.fst<VAR>h2 : (TensorPower.cast R M h) a.snd = b.snd<GOAL>a = b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>h : i = j<GOAL>⇑(TensorPower.cast R M h) = cast ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b) = (PiTensorProduct.tprod R) (Fin.append a b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>na nb nc : ℕ<VAR>a : ⨂[R]^na M<VAR>b : ⨂[R]^nb M<VAR>c : ⨂[R]^nc M<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>TensorPower.algebraMap₀ r = r • GradedMonoid.GOne.one
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorPower.algebraMap₀ 1 = GradedMonoid.GOne.one
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>r : R<VAR>a : ⨂[R]^n M<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) a) = r • a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>r : R<VAR>a : ⨂[R]^n M<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul a (TensorPower.algebraMap₀ r)) = r • a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r s : R<GOAL>(TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) (TensorPower.algebraMap₀ s)) = TensorPower.algebraMap₀ (r * s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>DirectSum.GAlgebra.toFun r = TensorPower.algebraMap₀ r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>Finite ι'<VAR>Finite κ'<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup M'<VAR>AddCommGroup N'<VAR>Module R M<VAR>Module R N<VAR>Module R M'<VAR>Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>f : M →ₗ[R] M'<VAR>g : N →ₗ[R] N'<GOAL>(LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.map f g) = Matrix.kroneckerMap (fun x x_1 => x * x_1) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>Finite ι'<VAR>Finite κ'<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup M'<VAR>AddCommGroup N'<VAR>Module R M<VAR>Module R N<VAR>Module R M'<VAR>Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>A : Matrix ι' ι R<VAR>B : Matrix κ' κ R<GOAL>(Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun x x_1 => x * x_1) A B) = TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.toLin bN bN') B)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<GOAL>(LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = Matrix.submatrix 1 Prod.swap id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>DecidableEq τ<VAR>Fintype ι<VAR>Fintype κ<VAR>Fintype τ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<GOAL>(LinearMap.toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))) ↑(TensorProduct.assoc R M N P) = Matrix.submatrix 1 id ⇑(Equiv.prodAssoc ι κ τ)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>x : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ<GOAL>(Algebra.TensorProduct.opAlgEquiv R S A B) x = MulOpposite.op ((TensorProduct.map ↑(MulOpposite.opLinearEquiv R).symm ↑(MulOpposite.opLinearEquiv R).symm) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>x : (A ⊗[R] B)ᵐᵒᵖ<GOAL>(Algebra.TensorProduct.opAlgEquiv R S A B).symm x = (TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R)) (MulOpposite.unop x)