ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieAlgebra.IsNilpotent R ↥(LieAlgebra.ad R L).range ↔ LieAlgebra.IsNilpotent R L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>I.lcs M 0 = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<GOAL>I.lcs M (k + 1) = ⁅I, I.lcs M k⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>k : ℕ<GOAL>⊤.lcs M k = LieModule.lowerCentralSeries R L M k
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>k : ℕ<GOAL>↑(I.lcs M k) = ↑(LieModule.lowerCentralSeries R (↥↑I) M k)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<GOAL>IsNilpotent ((LieAlgebra.ad R A) a)
<VAR>R : Type u<VAR>CommRing R<VAR>L : Type v<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>x : ↥K<VAR>h : IsNilpotent ((LieAlgebra.ad R L) ↑x)<GOAL>IsNilpotent ((LieAlgebra.ad R ↥K) x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>L : LieSubalgebra R A<VAR>x : ↥L<VAR>h : IsNilpotent ↑x<GOAL>IsNilpotent ((LieAlgebra.ad R ↥L) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>k : ℕ<GOAL>LieModule.lowerCentralSeries A (TensorProduct R A L) (TensorProduct R A M) k = LieSubmodule.baseChange A (LieModule.lowerCentralSeries R L M k)
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x y : L<GOAL>(LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).Monic
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x y : L<GOAL>(LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).natDegree = FiniteDimensional.finrank R M
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x y : L<VAR>r : R<GOAL>Polynomial.map (Polynomial.evalRingHom r) (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y) = LinearMap.charpoly ((LieModule.toEnd R L M) (r • y + x))
<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x y : L<VAR>i j : ℕ<VAR>hij : i + j = FiniteDimensional.finrank R M<GOAL>((LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).coeff i).natDegree ≤ j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>hLK : ↑(FiniteDimensional.finrank K L) ≤ Cardinal.mk K<VAR>U : LieSubalgebra K L<VAR>E : ↑{x | ∃ x_1 ∈ U, LieSubalgebra.engel K x_1 = x}<VAR>hUle : U ≤ ↑E<VAR>hmin : IsMin E<GOAL>IsBot E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>h : ↑(FiniteDimensional.finrank K L) ≤ Cardinal.mk K<GOAL>∃ x, (LieSubalgebra.engel K x).IsCartanSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>Module.Finite K L<VAR>Infinite K<GOAL>∃ x, (LieSubalgebra.engel K x).IsCartanSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>s t : A<VAR>x : L<VAR>m : M<GOAL>((LieAlgebra.ExtendScalars.bracket' R A L M) (s ⊗ₜ[R] x)) (t ⊗ₜ[R] m) = (s * t) ⊗ₜ[R] ⁅x, m⁆
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x : A ⊗[R] L<VAR>m : A ⊗[R] M<GOAL>⁅x, m⁆ = ((LieAlgebra.ExtendScalars.bracket' R A L M) x) m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>s t : A<VAR>x : L<VAR>y : M<GOAL>⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : A ⊗[R] L<GOAL>⁅x, x⁆ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>x y : A ⊗[R] L<VAR>z : A ⊗[R] M<GOAL>⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>x : L<GOAL>(LieModule.toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((LieModule.toEnd R L M) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>N : LieSubmodule R L M<GOAL>↑(LieSubmodule.baseChange A N) = Submodule.baseChange A ↑N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>N : LieSubmodule R L M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ N<GOAL>a ⊗ₜ[R] m ∈ LieSubmodule.baseChange A N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>N : LieSubmodule R L M<VAR>m : A ⊗[R] M<GOAL>m ∈ LieSubmodule.baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<GOAL>LieSubmodule.baseChange A ⊥ = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<GOAL>LieSubmodule.baseChange A ⊤ = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>CommRing A<VAR>Algebra R A<VAR>I : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.baseChange A ⁅I, N⁆ = ⁅LieSubmodule.baseChange A I, LieSubmodule.baseChange A N⁆
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>Semigroup G₁<VAR>Semigroup G₂<VAR>x y : G₁ × G₂<GOAL>x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>Semigroup G₁<VAR>Semigroup G₂<VAR>x₁ y₁ : G₁<VAR>x₂ y₂ : G₂<GOAL>(x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂
<VAR>ι : Type u_1<VAR>G : ι → Type u_4<VAR>(i : ι) → Semigroup (G i)<VAR>x y : (i : ι) → G i<GOAL>x ∣ y ↔ ∀ (i : ι), x i ∣ y i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<GOAL>Function.Injective AddConstEquiv.toEquiv
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e₁ e₂ : G ≃+c[a, b] H<VAR>h : ∀ (x : G), e₁ x = e₂ x<GOAL>e₁ = e₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e₁ e₂ : G ≃+c[a, b] H<GOAL>e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>⇑e.toEquiv = ⇑e
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>e.symm.symm = e
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>(AddConstEquiv.refl a).toEquiv = Equiv.refl G
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>∀ (a_1 : G), (AddConstEquiv.refl a) a_1 = a_1
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>(AddConstEquiv.refl a).symm = AddConstEquiv.refl a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>K : Type u_3<VAR>Add G<VAR>Add H<VAR>Add K<VAR>a : G<VAR>b : H<VAR>c : K<VAR>e₁ : G ≃+c[a, b] H<VAR>e₂ : H ≃+c[b, c] K<GOAL>(e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>K : Type u_3<VAR>Add G<VAR>Add H<VAR>Add K<VAR>a : G<VAR>b : H<VAR>c : K<VAR>e₁ : G ≃+c[a, b] H<VAR>e₂ : H ≃+c[b, c] K<GOAL>∀ (a_1 : G), (e₁.trans e₂) a_1 = e₂ (e₁ a_1)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>e.trans (AddConstEquiv.refl b) = e
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>(AddConstEquiv.refl a).trans e = e
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>e.trans e.symm = AddConstEquiv.refl a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>e : G ≃+c[a, b] H<GOAL>e.symm.trans e = AddConstEquiv.refl b
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>self : G ≃+c[a, a] G<GOAL>AddConstEquiv.toPerm self = self.toEquiv
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>self : G ≃+c[a, a] G<GOAL>AddConstEquiv.toAddConstMapHom self = self.toAddConstMap
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>∀ (a_1 : G ≃+c[a, a] G) (a_2 : G), ↑(AddConstEquiv.equivUnits a_1)⁻¹ a_2 = a_1⁻¹ a_2
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>u : (G →+c[a, a] G)ˣ<GOAL>⇑(AddConstEquiv.equivUnits.symm u).symm = ⇑↑u⁻¹
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>∀ (a_1 : G ≃+c[a, a] G) (a_2 : G), ↑(AddConstEquiv.equivUnits a_1) a_2 = a_1 a_2
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<VAR>u : (G →+c[a, a] G)ˣ<GOAL>⇑(AddConstEquiv.equivUnits.symm u) = ⇑↑u
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>AddCommGroup M<VAR>Module ℚ M<VAR>AddCommGroup M₂<VAR>Module ℚ M₂<GOAL>Function.Injective AddMonoidHom.toRatLinearMap
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>AddCommGroup M<VAR>Module ℚ M<VAR>AddCommGroup M₂<VAR>Module ℚ M₂<VAR>f : M →+ M₂<GOAL>⇑f.toRatLinearMap = ⇑f
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<VAR>u : αˣ<GOAL>↑u ∣ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a ∣ b * ↑u ↔ a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a * ↑u ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a ∣ ↑u * b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>↑u * a ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a u : α<VAR>hu : IsUnit u<GOAL>u ∣ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b u : α<VAR>hu : IsUnit u<GOAL>a ∣ b * u ↔ a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b u : α<VAR>hu : IsUnit u<GOAL>a * u ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>u : α<VAR>hu : IsUnit u<GOAL>IsPrimal u
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b u : α<VAR>hu : IsUnit u<GOAL>a ∣ u * b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b u : α<VAR>hu : IsUnit u<GOAL>u * a ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<GOAL>IsUnit x ↔ x ∣ 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<GOAL>IsUnit x ↔ ∀ (y : α), x ∣ y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<VAR>xy : x ∣ y<VAR>hu : IsUnit y<GOAL>IsUnit x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<VAR>h : a ∣ 1<GOAL>IsUnit a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : a ∣ b<GOAL>¬IsUnit b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<VAR>H : IsRelPrime x y<GOAL>IsRelPrime y x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<GOAL>IsRelPrime x y ↔ IsRelPrime y x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<GOAL>IsRelPrime x x ↔ IsUnit x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<VAR>h : IsUnit x<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<VAR>h : IsUnit y<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<GOAL>IsRelPrime 1 x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<GOAL>IsRelPrime x 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime (x * y) z<GOAL>IsRelPrime x z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime (x * y) z<GOAL>IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x (y * z)<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x (y * z)<GOAL>IsRelPrime x z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>h : IsRelPrime y z<VAR>dvd : x ∣ y<GOAL>IsRelPrime x z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>h : IsRelPrime z y<VAR>dvd : x ∣ y<GOAL>IsRelPrime z x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<VAR>H : IsRelPrime x y<VAR>d : x ∣ y<GOAL>IsUnit x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (x * y) z ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime y (x * z) ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (y * x) z ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime y (z * x) ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H1 : IsRelPrime x z<VAR>H2 : x ∣ y * z<VAR>h : IsPrimal x<GOAL>x ∣ y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H1 : IsRelPrime x y<VAR>H2 : x ∣ y * z<VAR>h : IsPrimal x<GOAL>x ∣ z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>hy : IsPrimal y<GOAL>x * y ∣ z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>hx : IsPrimal x<GOAL>x * y ∣ z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<VAR>H1 : IsRelPrime x z<VAR>H2 : x ∣ y * z<GOAL>x ∣ y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<VAR>H1 : IsRelPrime x y<VAR>H2 : x ∣ y * z<GOAL>x ∣ z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<VAR>H1 : IsRelPrime x z<VAR>H2 : IsRelPrime y z<GOAL>IsRelPrime (x * y) z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<VAR>H1 : IsRelPrime x y<VAR>H2 : IsRelPrime x z<GOAL>IsRelPrime x (y * z)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<GOAL>IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<GOAL>IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y z : α<VAR>DecompositionMonoid α<VAR>H : IsRelPrime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<GOAL>x * y ∣ z
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b : α<VAR>c : α<VAR>h : a * c = b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b : α<VAR>h : a ∣ b<GOAL>∃ c, b = a * c
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b : α<GOAL>a ∣ b ↔ ∃ c, b = a * c
<VAR>α : Type u_1<VAR>Semigroup α<VAR>P : Prop<VAR>a b : α<VAR>H₁ : a ∣ b<VAR>H₂ : ∀ (c : α), b = a * c → P<GOAL>P
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b c : α<GOAL>a ∣ b → b ∣ c → a ∣ c
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b : α<GOAL>a ∣ a * b
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b : α<VAR>h : a ∣ b<VAR>c : α<GOAL>a ∣ b * c
<VAR>α : Type u_1<VAR>Semigroup α<VAR>a b c : α<VAR>h : a * b ∣ c<GOAL>a ∣ c
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Semigroup M<VAR>Semigroup N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>a b : M<GOAL>a ∣ b → f a ∣ f b
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Semigroup M<VAR>Semigroup N<VAR>f : M →ₙ* N<VAR>a b : M<GOAL>a ∣ b → f a ∣ f b
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>a b : M<GOAL>a ∣ b → f a ∣ f b
<VAR>α : Type u_1<VAR>Semigroup α<GOAL>DecompositionMonoid α ↔ ∀ (a : α), IsPrimal a
<VAR>α : Type u_1<VAR>Semigroup α<VAR>self : DecompositionMonoid α<VAR>a : α<GOAL>IsPrimal a
<VAR>α : Type u_1<VAR>Semigroup α<VAR>DecompositionMonoid α<VAR>b c a : α<VAR>H : a ∣ b * c<GOAL>∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>a ∣ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>1 ∣ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : a = b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>m n : ℕ<VAR>a : α<VAR>h : m ≤ n<GOAL>a ^ m ∣ a ^ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>hab : a ∣ b<VAR>n : ℕ<GOAL>n ≠ 0 → a ∣ b ^ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ∣ a ^ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>b c : α<VAR>a : α<VAR>h : b ∣ c<GOAL>a * b ∣ a * c
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<VAR>c : α<VAR>h : c * a = b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<VAR>h : a ∣ b<GOAL>∃ c, b = c * a
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<GOAL>a ∣ b ↔ ∃ c, b = c * a
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<VAR>P : Prop<VAR>h₁ : a ∣ b<VAR>h₂ : ∀ (c : α), b = c * a → P<GOAL>P
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<GOAL>a ∣ b * a
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b : α<VAR>h : a ∣ b<VAR>c : α<GOAL>a ∣ c * b
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b c d : α<GOAL>a ∣ b → c ∣ d → a * c ∣ b * d
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>a b c : α<VAR>h : a * b ∣ c<GOAL>b ∣ c
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>DecompositionMonoid α<VAR>k m n : α<GOAL>k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>h : a ∣ b<VAR>c : α<GOAL>a * c ∣ b * c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>h : a ∣ b<VAR>n : ℕ<GOAL>a ^ n ∣ b ^ n
<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_6<VAR>S : Type u_7<VAR>DivisionSemiring R<VAR>DivisionSemiring S<VAR>Module R M<VAR>Module S M₂<VAR>n : ℕ<VAR>x : M<GOAL>f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>F : Type u_5<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_6<VAR>S : Type u_7<VAR>DivisionRing R<VAR>DivisionRing S<VAR>Module R M<VAR>Module S M₂<VAR>z : ℤ<VAR>x : M<GOAL>f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x
<VAR>E : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>AddCommMonoid E<VAR>DivisionSemiring R<VAR>DivisionSemiring S<VAR>Module R E<VAR>Module S E<VAR>n : ℕ<VAR>x : E<GOAL>(↑n)⁻¹ • x = (↑n)⁻¹ • x
<VAR>E : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>AddCommGroup E<VAR>DivisionRing R<VAR>DivisionRing S<VAR>Module R E<VAR>Module S E<VAR>n : ℤ<VAR>x : E<GOAL>(↑n)⁻¹ • x = (↑n)⁻¹ • x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>R : Type u_7<VAR>AddCommMonoid E<VAR>DivisionSemiring R<VAR>Monoid α<VAR>Module R E<VAR>DistribMulAction α E<VAR>n : ℕ<VAR>s : α<VAR>x : E<GOAL>(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>R : Type u_7<VAR>AddCommGroup E<VAR>DivisionRing R<VAR>Monoid α<VAR>Module R E<VAR>DistribMulAction α E<VAR>n : ℤ<VAR>s : α<VAR>x : E<GOAL>(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>f : α → R<VAR>g : α → M<GOAL>Function.support (f • g) ⊆ Function.support f
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>f : α → R<VAR>g : α → M<GOAL>Function.support (f • g) ⊆ Function.support g
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>g : α → M<VAR>hc : c ≠ 0<GOAL>Function.support (c • g) = Function.support g
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>f : α → R<VAR>g : α → M<GOAL>Function.support (f • g) = Function.support f ∩ Function.support g
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>a : R<VAR>f : α → M<GOAL>Function.support (a • f) ⊆ Function.support f
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<GOAL>s.indicator (fun a => r a • f a) a = r a • s.indicator f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<GOAL>(s.indicator fun a => r a • f a) = fun a => r a • s.indicator f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>s : Set α<VAR>r : R<VAR>f : α → M<VAR>a : α<GOAL>s.indicator (fun x => r • f x) a = r • s.indicator f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero M<VAR>SMulZeroClass R M<VAR>s : Set α<VAR>r : R<VAR>f : α → M<GOAL>(s.indicator fun x => r • f x) = fun x => r • s.indicator f x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<GOAL>s.indicator (fun a => r a • f a) a = s.indicator r a • f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<GOAL>(s.indicator fun a => r a • f a) = fun a => s.indicator r a • f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>m : M<VAR>a : α<GOAL>s.indicator (fun x => r x • m) a = s.indicator r a • m
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>s : Set α<VAR>r : α → R<VAR>m : M<GOAL>(s.indicator fun x => r x • m) = fun x => s.indicator r x • m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsLinearMap R fun x => x.1 + x.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsLinearMap R fun x => x.1 - x.2
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>S' : Type u_17<VAR>Monoid S'<VAR>DistribMulAction S' M<VAR>SMulCommClass R S' M<VAR>a : S'ᵈᵐᵃ<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>x : M<GOAL>(a • f) x = f (DomMulAct.mk.symm a • x)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>S' : Type u_17<VAR>Monoid S'<VAR>DistribMulAction S' M<VAR>SMulCommClass R S' M<VAR>a : S'<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>x : M<GOAL>(DomMulAct.mk a • f) x = f (a • x)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>S' : Type u_17<VAR>Monoid S'<VAR>DistribMulAction S' M<VAR>SMulCommClass R S' M<VAR>a : S'ᵈᵐᵃ<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>⇑(a • f) = a • ⇑f