ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>s : Set R<VAR>h : Module.IsTorsionBySet R M s<GOAL>Module.IsTorsionBySet R (M ⧸ N) s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R (M ⧸ s • ⊤) s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>Module.IsTorsionBy R (M ⧸ r • ⊤) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>Module.IsTorsionBySet R (M ⧸ I • ⊤) ↑I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>r : R<VAR>m : M<GOAL>(Ideal.Quotient.mk I) r • Submodule.Quotient.mk m = Submodule.Quotient.mk (r • m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>b : R<VAR>x : ↥(Submodule.torsionBySet R M ↑I)<GOAL>(Ideal.Quotient.mk I) b • x = b • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>a b : R<VAR>x : ↥(Submodule.torsionBy R M a)<GOAL>(Ideal.Quotient.mk (Ideal.span {a})) b • x = b • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>a b : R<VAR>x : ↥(Submodule.torsionBy R M a)<GOAL>(Ideal.Quotient.mk (Submodule.span R {a})) b • x = b • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>x : M<GOAL>x ∈ Submodule.torsion' R M S ↔ ∃ a, a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>x ∈ Submodule.torsion R M ↔ ∃ a, a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : S<VAR>x : ↥(Submodule.torsion' R M S)<GOAL>↑(s • x) = s • ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<GOAL>Module.IsTorsion' M S ↔ Submodule.torsion' R M S = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<GOAL>Module.IsTorsion' (↥(Submodule.torsion' R M S)) S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<GOAL>Submodule.torsion' R (↥(Submodule.torsion' R M S)) S = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.torsion R ↥(Submodule.torsion R M) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.IsTorsion R ↥(Submodule.torsion R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.IsTorsionBySet R M ↑⊤.annihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>↑⊤.annihilator ∩ ↑R⁰ ≠ ∅
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroDivisors R<VAR>Nontrivial R<GOAL>↑(Submodule.torsion R M) = {x | (Submodule.span R {x}).annihilator ≠ ⊥}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroDivisors R<VAR>Nontrivial R<GOAL>NoZeroSMulDivisors R M ↔ Submodule.torsion R M = ⊥
<VAR>G : Type u_3<VAR>AddCommGroup G<GOAL>(Submodule.torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Submodule.torsion R (M ⧸ Submodule.torsion R M) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>AddCommMonoid M<VAR>DistribMulAction R M<VAR>p : R<GOAL>Module.IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ n, p ^ n • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid R<VAR>AddCommMonoid M<VAR>DistribMulAction R M<VAR>p : R<VAR>hM : Module.IsTorsion' M ↥(Submonoid.powers p)<VAR>x : M<VAR>(n : ℕ) → Decidable (p ^ n • x = 0)<GOAL>p ^ Submodule.pOrder hM x • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>(x : M) → Decidable (x = 0)<VAR>p : R<VAR>hM : Module.IsTorsion' M ↥(Submonoid.powers p)<VAR>d : ℕ<VAR>hd : d ≠ 0<VAR>s : Fin d → M<VAR>hs : Submodule.span R (Set.range s) = ⊤<GOAL>∃ j, Module.IsTorsionBy R M (p ^ Submodule.pOrder hM (s j))
<VAR>R : Type w<VAR>CommRing R<VAR>a b : R<VAR>ha : a ∈ R⁰<GOAL>Submodule.torsionBy R (R ⧸ Submodule.span R {a * b}) a = Submodule.span R {(Ideal.Quotient.mk (Submodule.span R {a * b})) b}
<VAR>M : Type u_2<VAR>AddCommMonoid M<GOAL>AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M
<VAR>M : Type u_2<VAR>AddCommGroup M<GOAL>AddMonoid.IsTorsion M ↔ Module.IsTorsion ℤ M
<VAR>R : Type u_1<VAR>Mul R<VAR>StarMul R<VAR>a : R<VAR>ha : a ∈ Set.center R<GOAL>star a ∈ Set.center R
<VAR>R : Type u_1<VAR>Mul R<VAR>StarMul R<VAR>a : R<VAR>s : Set R<VAR>h : ∀ a ∈ s, star a ∈ s<VAR>ha : a ∈ s.centralizer<GOAL>star a ∈ s.centralizer
<VAR>R : Type u_1<VAR>Mul R<VAR>StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ (s ∪ star s).centralizer<GOAL>star a ∈ (s ∪ star s).centralizer
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>self : Module.Injective R Q<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>AddCommGroup Y<VAR>Module R X<VAR>Module R Y<VAR>f : X →ₗ[R] Y<GOAL>Function.Injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ h, ∀ (x : X), h (f x) = g x
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<GOAL>Module.Injective R Q ↔ ∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y] (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ h, ∀ (x : X), h (f x) = g x
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>inj : Module.Injective R Q<GOAL>CategoryTheory.Injective (ModuleCat.of R Q)
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>inj : CategoryTheory.Injective (ModuleCat.of R Q)<GOAL>Module.Injective R Q
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<GOAL>Module.Injective R Q ↔ CategoryTheory.Injective (ModuleCat.of R Q)
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>self : Module.Baer.ExtensionOf i f<GOAL>LinearMap.range i ≤ self.domain
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>self : Module.Baer.ExtensionOf i f<VAR>m : M<GOAL>f m = ↑self.toLinearPMap ⟨i m, ⋯⟩
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>a b : Module.Baer.ExtensionOf i f<VAR>domain_eq : a.domain = b.domain<VAR>to_fun_eq : ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y<GOAL>a = b
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>a b : Module.Baer.ExtensionOf i f<GOAL>a = b ↔ ∃ (_ : a.domain = b.domain), ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>c : Set (Module.Baer.ExtensionOf i f)<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<GOAL>IsChain (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) '' c)
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>c : Set (Module.Baer.ExtensionOf i f)<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>hnonempty : c.Nonempty<VAR>a : Module.Baer.ExtensionOf i f<VAR>ha : a ∈ c<GOAL>a ≤ Module.Baer.ExtensionOf.max hchain hnonempty
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>a : Module.Baer.ExtensionOf i f<GOAL>Module.Baer.extensionOfMax i f ≤ a → a = Module.Baer.extensionOfMax i f
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)<GOAL>∃ a b, ↑x = ↑a + b • y
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)<GOAL>↑x = ↑(Module.Baer.ExtensionOfMaxAdjoin.fst i x) + Module.Baer.ExtensionOfMaxAdjoin.snd i x • y
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<VAR>x : R<VAR>mem : x ∈ Module.Baer.ExtensionOfMaxAdjoin.ideal i f y<GOAL>(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) x = (Module.Baer.ExtensionOfMaxAdjoin.idealTo i f y) ⟨x, mem⟩
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<VAR>r : R<VAR>eq1 : r • y = 0<GOAL>(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = 0
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<VAR>r r' : R<VAR>eq1 : r • y = r' • y<GOAL>(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r'
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<VAR>r : R<VAR>hr : r • y ∈ (Module.Baer.extensionOfMax i f).domain<GOAL>(Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = ↑(Module.Baer.extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<VAR>x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)<VAR>a : ↥(Module.Baer.extensionOfMax i f).domain<VAR>r : R<VAR>eq1 : ↑x = ↑a + r • y<GOAL>Module.Baer.ExtensionOfMaxAdjoin.extensionToFun i f h x = ↑(Module.Baer.extensionOfMax i f).toLinearPMap a + (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<VAR>y : N<GOAL>Module.Baer.extensionOfMax i f ≤ Module.Baer.extensionOfMaxAdjoin i f h y
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>Fact (Function.Injective ⇑i)<VAR>h : Module.Baer R Q<GOAL>(Module.Baer.extensionOfMax i f).domain = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>h : Module.Baer R Q<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>g : M →ₗ[R] Q<GOAL>∃ h, h ∘ₗ f = g
<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>h : Module.Baer ℤ Q<VAR>f : M →+ N<VAR>hf : Function.Injective ⇑f<VAR>g : M →+ Q<GOAL>∃ h, h.comp f = g
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>h : Module.Baer R Q<GOAL>Module.Injective R Q
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>Small.{v, u} R<VAR>inj : Module.Injective R Q<GOAL>Module.Baer R Q
<VAR>R : Type u<VAR>Ring R<VAR>Q : Type v<VAR>AddCommGroup Q<VAR>Module R Q<VAR>Small.{v, u} R<GOAL>Module.Baer R Q ↔ Module.Injective R Q
<VAR>R : Type u<VAR>Ring R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<VAR>inj : Module.Injective R M<GOAL>Module.Injective R (ULift.{v', v} M)
<VAR>R : Type u<VAR>Ring R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>inj : Module.Injective R (ULift.{v', v} M)<GOAL>Module.Injective R M
<VAR>R : Type u<VAR>Ring R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Injective R M ↔ Module.Injective R (ULift.{v', v} M)
<VAR>R : Type uR<VAR>Ring R<VAR>Small.{uM, uR} R<VAR>M : Type uM<VAR>AddCommGroup M<VAR>Module R M<VAR>inj : Module.Injective R M<VAR>P : Type uP<VAR>AddCommGroup P<VAR>Module R P<VAR>P' : Type uP'<VAR>AddCommGroup P'<VAR>Module R P'<VAR>f : P →ₗ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>g : P →ₗ[R] M<GOAL>∃ h, h ∘ₗ f = g
<VAR>α : Type u_1<VAR>NonUnitalNonAssocSemiring α<VAR>StarRing α<VAR>f : CentroidHom α<VAR>a : α<GOAL>(star f) a = star (f (star a))
<VAR>α : Type u_1<VAR>NonUnitalNonAssocSemiring α<VAR>StarRing α<VAR>z : ↥(NonUnitalStarSubsemiring.center α)<GOAL>star (CentroidHom.centerToCentroidCenter z) = CentroidHom.centerToCentroidCenter (star z)
<VAR>α : Type u_1<VAR>NonUnitalNonAssocSemiring α<VAR>StarRing α<VAR>z : ↥(NonUnitalStarSubsemiring.center α)<VAR>a : α<GOAL>(CentroidHom.starCenterToCentroid z) a = ↑z * a
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>StarRing α<VAR>a : ↥(NonUnitalStarSubsemiring.center α)<GOAL>CentroidHom.starCenterIsoCentroid a = CentroidHom.starCenterToCentroid a
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>StarRing α<VAR>T : CentroidHom α<GOAL>↑(CentroidHom.starCenterIsoCentroid.symm T) = T 1
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>Star R<VAR>SetLike S R<VAR>self : StarMemClass S R<VAR>s : S<VAR>r : R<GOAL>r ∈ s → star r ∈ s
<VAR>R : Type u<VAR>S : Type w<VAR>Star R<VAR>SetLike S R<VAR>hS : StarMemClass S R<VAR>s : S<VAR>x : ↥s<GOAL>↑(star x) = star ↑x
<VAR>R : Type u<VAR>self : InvolutiveStar R<GOAL>Function.Involutive star
<VAR>R : Type u<VAR>InvolutiveStar R<VAR>r : R<GOAL>star (star r) = r
<VAR>R : Type u<VAR>InvolutiveStar R<GOAL>Function.Injective star
<VAR>R : Type u<VAR>InvolutiveStar R<VAR>x y : R<GOAL>star x = star y ↔ x = y
<VAR>R : Type u<VAR>InvolutiveStar R<VAR>r s : R<VAR>h : r = star s<GOAL>s = star r
<VAR>R : Type u<VAR>InvolutiveStar R<VAR>r s : R<GOAL>r = star s ↔ s = star r
<VAR>R : Type u<VAR>InvolutiveStar R<VAR>r s : R<GOAL>star r = s ↔ star s = r
<VAR>R : Type u<VAR>Star R<VAR>self : TrivialStar R<VAR>r : R<GOAL>star r = r
<VAR>R : Type u<VAR>Mul R<VAR>self : StarMul R<VAR>r s : R<GOAL>star (r * s) = star s * star r
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x y : R<GOAL>star (star x * y) = star y * x
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x y : R<GOAL>star (x * star y) = y * star x
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x y z : R<GOAL>SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x y : R<GOAL>Commute (star x) (star y) ↔ Commute x y
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x y : R<GOAL>Commute (star x) y ↔ Commute x (star y)
<VAR>R : Type u<VAR>CommSemigroup R<VAR>StarMul R<VAR>x y : R<GOAL>star (x * y) = star x * star y
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>starMulEquiv x = MulOpposite.op (star x)
<VAR>R : Type u<VAR>CommSemigroup R<VAR>StarMul R<GOAL>∀ (a : R), starMulAut a = star a
<VAR>R : Type u<VAR>MulOneClass R<VAR>StarMul R<GOAL>star 1 = 1
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>x : R<VAR>n : ℕ<GOAL>star (x ^ n) = star x ^ n
<VAR>R : Type u<VAR>Group R<VAR>StarMul R<VAR>x : R<GOAL>star x⁻¹ = (star x)⁻¹
<VAR>R : Type u<VAR>Group R<VAR>StarMul R<VAR>x : R<VAR>z : ℤ<GOAL>star (x ^ z) = star x ^ z
<VAR>R : Type u<VAR>CommGroup R<VAR>StarMul R<VAR>x y : R<GOAL>star (x / y) = star x / star y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<GOAL>star x = x
<VAR>R : Type u<VAR>AddMonoid R<VAR>self : StarAddMonoid R<VAR>r s : R<GOAL>star (r + s) = star r + star s
<VAR>R : Type u<VAR>AddMonoid R<VAR>StarAddMonoid R<GOAL>∀ (a : R), starAddEquiv a = star a
<VAR>R : Type u<VAR>AddMonoid R<VAR>StarAddMonoid R<GOAL>star 0 = 0
<VAR>R : Type u<VAR>AddMonoid R<VAR>StarAddMonoid R<VAR>x : R<GOAL>star x = 0 ↔ x = 0
<VAR>R : Type u<VAR>AddMonoid R<VAR>StarAddMonoid R<VAR>x : R<GOAL>star x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>r : R<GOAL>star (-r) = -star r
<VAR>R : Type u<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>r s : R<GOAL>star (r - s) = star r - star s
<VAR>R : Type u<VAR>AddMonoid R<VAR>StarAddMonoid R<VAR>x : R<VAR>n : ℕ<GOAL>star (n • x) = n • star x
<VAR>R : Type u<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>x : R<VAR>n : ℤ<GOAL>star (n • x) = n • star x
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>self : StarRing R<VAR>r s : R<GOAL>star (r + s) = star r + star s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>StarRing R<VAR>x : R<GOAL>starRingEquiv x = MulOpposite.op (star x)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>n : ℕ<GOAL>star ↑n = ↑n
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>star (OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>Ring R<VAR>StarRing R<VAR>z : ℤ<GOAL>star ↑z = ↑z
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<GOAL>∀ (a : R), starRingAut a = star a
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>x : R<GOAL>(starRingEnd R) x = star x
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>x : R<GOAL>(starRingEnd R) ((starRingEnd R) x) = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>S : Type u_1<VAR>NonAssocSemiring S<VAR>f : S →+* R<GOAL>star f = (starRingEnd R).comp f
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>S : Type u_1<VAR>NonAssocSemiring S<VAR>f : S →+* R<VAR>s : S<GOAL>(star f) s = star (f s)
<VAR>R : Type u<VAR>CommSemiring R<VAR>StarRing R<VAR>TrivialStar R<VAR>a : R<GOAL>(starRingEnd R) a = a
<VAR>R : Type u<VAR>DivisionSemiring R<VAR>StarRing R<VAR>x : R<GOAL>star x⁻¹ = (star x)⁻¹
<VAR>R : Type u<VAR>DivisionSemiring R<VAR>StarRing R<VAR>x : R<VAR>z : ℤ<GOAL>star (x ^ z) = star x ^ z
<VAR>R : Type u<VAR>Semifield R<VAR>StarRing R<VAR>x y : R<GOAL>star (x / y) = star x / star y
<VAR>R : Type u<VAR>A : Type v<VAR>Star R<VAR>Star A<VAR>SMul R A<VAR>self : StarModule R A<VAR>r : R<VAR>a : A<GOAL>star (r • a) = star r • star a
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>S : outParam (Type u_3)<VAR>Star R<VAR>Star S<VAR>FunLike F R S<VAR>self : StarHomClass F R S<VAR>f : F<VAR>r : R<GOAL>f (star r) = star (f r)
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>u : Rˣ<GOAL>↑(star u) = star ↑u
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>u : Rˣ<GOAL>↑(star u)⁻¹ = star ↑u⁻¹
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>a : R<GOAL>IsUnit a → IsUnit (star a)
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>a : R<GOAL>IsUnit (star a) ↔ IsUnit a
<VAR>R : Type u<VAR>Semiring R<VAR>StarRing R<VAR>a : R<GOAL>Ring.inverse (star a) = star (Ring.inverse a)
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>r : R<VAR>Invertible r<VAR>Invertible (star r)<GOAL>star ⅟r = ⅟(star r)
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<VAR>hx : IsLeftRegular x<GOAL>IsRightRegular (star x)
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<VAR>hx : IsRightRegular x<GOAL>IsLeftRegular (star x)
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<VAR>hx : IsRegular x<GOAL>IsRegular (star x)
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>IsRightRegular (star x) ↔ IsLeftRegular x
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>IsLeftRegular (star x) ↔ IsRightRegular x
<VAR>R : Type u<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>IsRegular (star x) ↔ IsRegular x
<VAR>R : Type u<VAR>Star R<VAR>r : Rᵐᵒᵖ<GOAL>MulOpposite.unop (star r) = star (MulOpposite.unop r)
<VAR>R : Type u<VAR>Star R<VAR>r : R<GOAL>MulOpposite.op (star r) = star (MulOpposite.op r)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Star (f i)<VAR>x : (i : I) → f i<VAR>i : I<GOAL>star x i = star (x i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Star (f i)<VAR>x : (i : I) → f i<GOAL>star x = fun i => star (x i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → AddMonoid (f i)<VAR>(i : I) → StarAddMonoid (f i)<VAR>DecidableEq I<VAR>i : I<VAR>a : f i<GOAL>Pi.single i (star a) = star (Pi.single i a)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CommSemiring (α i)<VAR>(i : ι) → StarRing (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<GOAL>(starRingEnd ((i : ι) → α i)) f i = (starRingEnd (α i)) (f i)
<VAR>I : Type u<VAR>f : I → Type v<VAR>(i : I) → Star (f i)<VAR>DecidableEq I<VAR>h : (i : I) → f i<VAR>i : I<VAR>a : f i<GOAL>Function.update (star h) i (star a) = star (Function.update h i a)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>α : Type u_3<VAR>x : I → α<VAR>y : J → α<VAR>Star α<GOAL>star (Sum.elim x y) = Sum.elim (star x) (star y)
<VAR>R : Type u<VAR>S : Type v<VAR>Star R<VAR>Star S<VAR>x : R × S<GOAL>(star x).1 = star x.1
<VAR>R : Type u<VAR>S : Type v<VAR>Star R<VAR>Star S<VAR>x : R × S<GOAL>(star x).2 = star x.2
<VAR>R : Type u<VAR>S : Type v<VAR>Star R<VAR>Star S<VAR>x : R × S<GOAL>star x = (star x.1, star x.2)
<VAR>R : Type u<VAR>Monoid R<VAR>StarMul R<VAR>u : Rˣ<GOAL>(Units.embedProduct R) (star u) = star ((Units.embedProduct R) u)
<VAR>R : Type u<VAR>CommRing R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>a : R<VAR>h : Irreducible a<GOAL>IsSemisimpleModule R ↥(Submodule.torsionBy R M a)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>DirectSum.IsInternal fun p => Submodule.torsionBy R M (Submodule.IsPrincipal.generator ↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>∃ ι x x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i => Submodule.torsionBy R M (p i ^ e i)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : Module.IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<GOAL>Ideal.torsionOf R M x = Ideal.span {p ^ Submodule.pOrder hM x}