Commit 2023-04-03 20:29 f1aa4719

View on Github →

feat: port RingTheory.FiniteType (#3241)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FiniteType.lean

added theorem AddMonoidAlgebra.exists_finset_adjoin_eq_top

added theorem AddMonoidAlgebra.fg_of_finiteType

added theorem AddMonoidAlgebra.finiteType_iff_fg

added theorem AddMonoidAlgebra.finiteType_iff_group_fg

added theorem AddMonoidAlgebra.mem_adjoin_support

added theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure

added theorem AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure

added theorem AddMonoidAlgebra.of'_mem_span

added theorem AddMonoidAlgebra.support_gen_of_gen'

added theorem AddMonoidAlgebra.support_gen_of_gen

added theorem AlgHom.Finite.finiteType

added theorem AlgHom.FiniteType.comp

added theorem AlgHom.FiniteType.comp_surjective

added theorem AlgHom.FiniteType.id

added theorem AlgHom.FiniteType.of_comp_finiteType

added theorem AlgHom.FiniteType.of_surjective

added def AlgHom.FiniteType

added theorem Algebra.FiniteType.equiv

added theorem Algebra.FiniteType.iff_quotient_mvPolynomial''

added theorem Algebra.FiniteType.iff_quotient_mvPolynomial'

added theorem Algebra.FiniteType.iff_quotient_mvPolynomial

added theorem Algebra.FiniteType.isNoetherianRing

added theorem Algebra.FiniteType.of_restrictScalars_finiteType

added theorem Algebra.FiniteType.of_surjective

added theorem Algebra.FiniteType.self

added theorem Algebra.FiniteType.trans

added theorem Module.Finite.injective_of_surjective_endomorphism

added theorem MonoidAlgebra.exists_finset_adjoin_eq_top

added theorem MonoidAlgebra.fg_of_finiteType

added theorem MonoidAlgebra.finiteType_iff_fg

added theorem MonoidAlgebra.finiteType_iff_group_fg

added theorem MonoidAlgebra.mem_adjoin_support

added theorem MonoidAlgebra.mem_closure_of_mem_span_closure

added theorem MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure

added theorem MonoidAlgebra.of_mem_span_of_iff

added theorem MonoidAlgebra.support_gen_of_gen'

added theorem MonoidAlgebra.support_gen_of_gen

added theorem RingHom.Finite.finiteType

added theorem RingHom.FiniteType.comp

added theorem RingHom.FiniteType.comp_surjective

added theorem RingHom.FiniteType.id

added theorem RingHom.FiniteType.of_comp_finiteType

added theorem RingHom.FiniteType.of_finite

added theorem RingHom.FiniteType.of_surjective

added def RingHom.FiniteType

added theorem Subalgebra.fg_iff_finiteType

added theorem modulePolynomialOfEndo.isScalarTower

added def modulePolynomialOfEndo

added theorem modulePolynomialOfEndo_smul_def