instance fixedPoints_isInvariant {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {G : Type u_3} [Group G] [MulSemiringAction G A] [SMulCommClass G R A] : Algebra.IsInvariant (↥(FixedPoints.subalgebra R A G)) A G

theorem hilbert_noether_integral {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G A] [SMulCommClass G R A] : Algebra.IsIntegral (↥(FixedPoints.subalgebra R A G)) A

theorem hilbert_noether_module_finite {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.FiniteType R A] : Module.Finite (↥(FixedPoints.subalgebra R A G)) A

theorem hilbert_noether_fg {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G A] [SMulCommClass G R A] [IsNoetherianRing R] [Algebra.FiniteType R A] : Algebra.FiniteType R ↥(FixedPoints.subalgebra R A G)