ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : α →+* β<GOAL>∀ (a : αᵐᵒᵖ), (RingHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))
<VAR>α : Type u_1<VAR>NonAssocRing α<VAR>m n : ℤ<GOAL>↑(m * n) = ↑m * ↑n
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℤ<VAR>m : ℕ<GOAL>↑(n ^ m) = ↑n ^ m
<VAR>n : ℤ<GOAL>Odd n ↔ n % 2 = 1
<VAR>n : ℤ<GOAL>¬Odd n ↔ n % 2 = 0
<VAR>n : ℤ<GOAL>Even n ↔ ¬Odd n
<VAR>n : ℤ<GOAL>Odd n ↔ ¬Even n
<VAR>n : ℤ<GOAL>Even n ∨ Odd n
<VAR>n : ℤ<GOAL>∃ k, n = 2 * k ∨ n = 2 * k + 1
<VAR>n : ℤ<GOAL>Xor' (Even n) (Odd n)
<VAR>n : ℤ<GOAL>∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
<VAR>n : ℤ<GOAL>¬Even (2 * n + 1)
<VAR>m n : ℤ<VAR>h : Odd (m * n)<GOAL>Odd m
<VAR>m n : ℤ<VAR>h : Odd (m * n)<GOAL>Odd n
<VAR>m : ℤ<VAR>n : ℕ<GOAL>Odd (m ^ n) ↔ Odd m ∨ n = 0
<VAR>m : ℤ<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Odd (m ^ n) ↔ Odd m
<VAR>m n : ℤ<VAR>h : Odd (m + n)<GOAL>m ≠ n
<VAR>n : ℤ<GOAL>Even (n * (n + 1))
<VAR>n : ℤ<GOAL>Even (n * (n - 1))
<VAR>n : ℕ<GOAL>Odd ↑n ↔ Odd n
<VAR>n : ℤ<GOAL>Even n.natAbs ↔ Even n
<VAR>n : ℤ<GOAL>Odd n.natAbs ↔ Odd n
<VAR>a b : ℤ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>4 ∣ a + b ∨ 4 ∣ a - b
<VAR>n : ℤ<GOAL>Odd n → 2 * (n / 2) + 1 = n
<VAR>n : ℤ<GOAL>Odd n → n / 2 * 2 + 1 = n
<VAR>n : ℤ<GOAL>Odd n → 1 + n / 2 * 2 = n
<VAR>n : ℤ<VAR>h : Odd n<GOAL>2 * (n / 2) = n - 1
<VAR>n : ℕ<GOAL>IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x₁ x₂ y₁ y₂ : R<GOAL>(x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>x₁ x₂ y₁ y₂ n : R<GOAL>(x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<GOAL>a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<GOAL>a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R<GOAL>(x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) = (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 + (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 + (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R<GOAL>(x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) = (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 + (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 + (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 + (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 + (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 + (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 + (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2
<VAR>M : Type u_1<VAR>Monoid M<VAR>F : Type u_2<VAR>DivisionRing F<VAR>MulSemiringAction M F<VAR>x : M<VAR>m : F<GOAL>x • m⁻¹ = (x • m)⁻¹
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>S : Subring R<VAR>self : IsInvariantSubring M S<VAR>m : M<VAR>x : R<GOAL>x ∈ S → m • x ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>R' : Type u_2<VAR>Ring R'<VAR>MulSemiringAction M R'<VAR>U : Subring R'<VAR>IsInvariantSubring M U<GOAL>⇑(IsInvariantSubring.subtypeHom M U) = Subtype.val
<VAR>M : Type u_1<VAR>Monoid M<VAR>R' : Type u_2<VAR>Ring R'<VAR>MulSemiringAction M R'<VAR>U : Subring R'<VAR>IsInvariantSubring M U<GOAL>(IsInvariantSubring.subtypeHom M U).toRingHom = U.subtype
<VAR>R : Type u_2<VAR>OrderedRing R<VAR>s : Subring R<GOAL>↑s.orderedSubtype = s.subtype
<VAR>G : Type u_1<VAR>Group G<VAR>R : Type u_2<VAR>Semiring R<VAR>MulSemiringAction G R<VAR>x : G<GOAL>∀ (a : R), (MulSemiringAction.toRingEquiv G R x) a = x • a
<VAR>G : Type u_1<VAR>Group G<VAR>R : Type u_2<VAR>Semiring R<VAR>MulSemiringAction G R<VAR>x : G<GOAL>∀ (a : R), (MulSemiringAction.toRingEquiv G R x).symm a = x⁻¹ • a
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>self : A ≃ₐ[R] B<VAR>r : R<GOAL>self.toFun ((algebraMap R A) r) = (algebraMap R B) r
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>A : outParam (Type u_3)<VAR>B : outParam (Type u_4)<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>EquivLike F A B<VAR>self : AlgEquivClass F R A B<VAR>f : F<VAR>r : R<GOAL>f ((algebraMap R A) r) = (algebraMap R B) r
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>F : Type u_1<VAR>EquivLike F A₁ A₂<VAR>AlgEquivClass F R A₁ A₂<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f g : A₁ ≃ₐ[R] A₂<VAR>h : ∀ (a : A₁), f a = g a<GOAL>f = g
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ ≃ₐ[R] A₂<VAR>x x' : A₁<GOAL>x = x' → f x = f x'
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f g : A₁ ≃ₐ[R] A₂<VAR>h : f = g<VAR>x : A₁<GOAL>f x = g x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f g : A₁ ≃ₐ[R] A₂<GOAL>f = g ↔ ∀ (x : A₁), f x = g x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Injective fun e => ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>toFun : A₁ → A₂<VAR>invFun : A₂ → A₁<VAR>left_inv : Function.LeftInverse invFun toFun<VAR>right_inv : Function.RightInverse invFun toFun<VAR>map_mul : ∀ (x y : A₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x * y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x * { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y<VAR>map_add : ∀ (x y : A₁), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun (x + y) = { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun x + { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun y<VAR>commutes : ∀ (r : R), { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r<GOAL>⇑{ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes } = toFun
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e' : A₂ → A₁<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : A₁), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A₁), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (r : R), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e.toEquiv = ↑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e.toRingEquiv = ↑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>↑↑e = ↑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>⇑↑e = ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>⇑e.toRingEquiv = ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Injective RingEquivClass.toRingEquiv
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x y : A₁<GOAL>e (x + y) = e x + e y
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e 0 = 0
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x y : A₁<GOAL>e (x * y) = e x * e y
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e 1 = 1
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>r : R<GOAL>e ((algebraMap R A₁) r) = (algebraMap R A₂) r
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>r : R<VAR>x : A₁<GOAL>e (r • x) = r • e x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>ι : Type u_1<VAR>f : ι → A₁<VAR>s : Finset ι<GOAL>e (∑ x ∈ s, f x) = ∑ x ∈ s, e (f x)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>α : Type u_1<VAR>Zero α<VAR>ι : Type u_2<VAR>f : ι →₀ α<VAR>g : ι → α → A₁<GOAL>e (f.sum g) = f.sum fun i b => e (g i b)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>↑e = ↑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Injective AlgHomClass.toAlgHom
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>↑↑e = ↑↑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₁<VAR>n : ℕ<GOAL>e (x ^ n) = e x ^ n
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>Function.Injective ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>Function.Surjective ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>Function.Bijective ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>↑AlgEquiv.refl = AlgHom.id R A₁
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>⇑AlgEquiv.refl = id
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>F : Type u_1<VAR>EquivLike F A₁ A₂<VAR>AlgEquivClass F R A₁ A₂<VAR>f : F<VAR>x : A₂<GOAL>f ((↑f).symm x) = x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>F : Type u_1<VAR>EquivLike F A₁ A₂<VAR>AlgEquivClass F R A₁ A₂<VAR>f : F<VAR>x : A₁<GOAL>(↑f).symm (f x) = x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>(↑e).symm = ↑e.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e.invFun = ⇑e.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e.symm.symm = e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Bijective AlgEquiv.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>f : A₂ → A₁<VAR>h₁ : Function.LeftInverse (⇑e) f<VAR>h₂ : Function.RightInverse (⇑e) f<VAR>h₃ : ∀ (x y : A₂), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A₂), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (r : R), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r<GOAL>{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ → A₂<VAR>f' : A₂ → A₁<VAR>h₁ : Function.LeftInverse f' f<VAR>h₂ : Function.RightInverse f' f<VAR>h₃ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A₁), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (r : R), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r<GOAL>{ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ }.symm = let __src := AlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅; { toFun := f', invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>AlgEquiv.refl.symm = AlgEquiv.refl
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>f : A₁ ≃ₐ[R] A₁<GOAL>(↑f).symm = ↑f.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>↑e.symm = (↑e).symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₂<GOAL>e (e.symm x) = x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₁<GOAL>e.symm (e x) = x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>e₁ : A₁ ≃ₐ[R] A₂<VAR>e₂ : A₂ ≃ₐ[R] A₃<VAR>x : A₃<GOAL>(e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>e₁ : A₁ ≃ₐ[R] A₂<VAR>e₂ : A₂ ≃ₐ[R] A₃<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>e₁ : A₁ ≃ₐ[R] A₂<VAR>e₂ : A₂ ≃ₐ[R] A₃<VAR>x : A₁<GOAL>(e₁.trans e₂) x = e₂ (e₁ x)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>(↑e).comp ↑e.symm = AlgHom.id R A₂
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>(↑e.symm).comp ↑e = AlgHom.id R A₁
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>Function.LeftInverse ⇑e.symm ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>Function.RightInverse ⇑e.symm ⇑e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>f : A₁ →ₐ[R] A₂<GOAL>(e₁.arrowCongr e₂) f = ((↑e₂).comp f).comp ↑e₁.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Semiring A₃'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>Algebra R A₃'<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>e₃ : A₃ ≃ₐ[R] A₃'<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₃<GOAL>(e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>AlgEquiv.refl.arrowCongr AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Semiring A₃'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>Algebra R A₃'<VAR>e₁ : A₁ ≃ₐ[R] A₂<VAR>e₁' : A₁' ≃ₐ[R] A₂'<VAR>e₂ : A₂ ≃ₐ[R] A₃<VAR>e₂' : A₂' ≃ₐ[R] A₃'<GOAL>(e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<GOAL>(e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e' : A₁' ≃ₐ[R] A₂'<VAR>ψ : A₁ ≃ₐ[R] A₁'<GOAL>(e.equivCongr e') ψ = e.symm.trans (ψ.trans e')
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₁' : Type uA₁'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₁'<VAR>Algebra R A₁<VAR>Algebra R A₁'<GOAL>AlgEquiv.refl.equivCongr AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁')
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e' : A₁' ≃ₐ[R] A₂'<GOAL>(e.equivCongr e').symm = e.symm.equivCongr e'.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Semiring A₁'<VAR>Semiring A₂'<VAR>Semiring A₃'<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>Algebra R A₁'<VAR>Algebra R A₂'<VAR>Algebra R A₃'<VAR>e₁₂ : A₁ ≃ₐ[R] A₂<VAR>e₁₂' : A₁' ≃ₐ[R] A₂'<VAR>e₂₃ : A₂ ≃ₐ[R] A₃<VAR>e₂₃' : A₂' ≃ₐ[R] A₃'<GOAL>(e₁₂.equivCongr e₁₂').trans (e₂₃.equivCongr e₂₃') = (e₁₂.trans e₂₃).equivCongr (e₁₂'.trans e₂₃')
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : f.comp g = AlgHom.id R A₂<VAR>h₂ : g.comp f = AlgHom.id R A₁<VAR>a : A₂<GOAL>(AlgEquiv.ofAlgHom f g h₁ h₂).symm a = g a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : f.comp g = AlgHom.id R A₂<VAR>h₂ : g.comp f = AlgHom.id R A₁<VAR>a : A₁<GOAL>(AlgEquiv.ofAlgHom f g h₁ h₂) a = f a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : f.comp g = AlgHom.id R A₂<VAR>h₂ : g.comp f = AlgHom.id R A₁<GOAL>↑(AlgEquiv.ofAlgHom f g h₁ h₂) = f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ ≃ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : (↑f).comp g = AlgHom.id R A₂<VAR>h₂ : g.comp ↑f = AlgHom.id R A₁<GOAL>AlgEquiv.ofAlgHom (↑f) g h₁ h₂ = f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : f.comp g = AlgHom.id R A₂<VAR>h₂ : g.comp f = AlgHom.id R A₁<GOAL>(AlgEquiv.ofAlgHom f g h₁ h₂).symm = AlgEquiv.ofAlgHom g f h₂ h₁
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>hf : Function.Bijective ⇑f<GOAL>⇑(AlgEquiv.ofBijective f hf) = ⇑f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>hf : Function.Bijective ⇑f<VAR>a : A₁<GOAL>(AlgEquiv.ofBijective f hf) a = f a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>a : A₁<GOAL>e.toLinearEquiv a = e a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>AlgEquiv.refl.toLinearEquiv = LinearEquiv.refl R A₁
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>e.toLinearEquiv.symm = e.symm.toLinearEquiv