JacobsonNoether

📁 Source: Mathlib/FieldTheory/JacobsonNoether.lean

Statistics

Metric	Count
Definitions	0
Theorems exist_pow_eq_zero_of_le, exists_pow_mem_center_of_inseparable, exists_pow_mem_center_of_inseparable', exists_separable_and_not_isCentral, exists_separable_and_not_isCentral'	5
Total	5

JacobsonNoether

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exist_pow_eq_zero_of_le 📖	mathematical	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Nat.iterate DFunLike.coe Module.End Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center CommSemiring.toSemiring CommRing.toCommSemiring Subring.instCommRingSubtypeMemCenter AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing LieAlgebra.toModule LieAlgebra.ofAssociativeAlgebra Algebra.instSubtypeMemSubringCenter LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieAlgebra.ad Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing	—	smulCommClass_self IsScalarTower.left exists_pow_mem_center_of_inseparable' Algebra.to_smulCommClass IsScalarTower.right LieAlgebra.ad_eq_lmul_left_sub_lmul_right Module.End.pow_apply Pi.sub_apply sub_pow_expChar_pow_of_commute instExpCharLinearMapSubtypeMemSubringCenterId LinearMap.commute_mulLeft_right LinearMap.sub_apply LinearMap.pow_mulLeft LinearMap.mulLeft_apply LinearMap.pow_mulRight LinearMap.mulRight_apply Pi.zero_apply Subring.mem_center_iff sub_eq_zero_of_eq Function.iterate_add Pi.comp_zero iterate_map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Function.const_zero
exists_pow_mem_center_of_inseparable 📖	mathematical	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Nat.instMonoid	—	isPurelyInseparable_iff_pow_mem DivisionRing.isDomain ExpChar.expChar_center_iff Algebra.IsAlgebraic.isIntegral RingHom.mem_range Subalgebra.range_subset Set.mem_of_subset_of_mem Set.mem_range
exists_pow_mem_center_of_inseparable' 📖	mathematical	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Nat.instMonoid	—	exists_pow_mem_center_of_inseparable pow_one pow_zero
exists_separable_and_not_isCentral 📖	mathematical	—	Subring Ring.toNonAssocRing DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center IsSeparable Subring.instCommRingSubtypeMemCenter Algebra.instSubtypeMemSubringCenter	—	ExpChar.exists DivisionRing.isDomain Mathlib.Tactic.Push.not_and_eq Subring.eq_top_iff' Subring.zero_mem smulCommClass_self IsScalarTower.left Subring.mem_center_iff exist_pow_eq_zero_of_le expChar_pow_pos Pi.zero_apply Nat.find_spec Nat.find_min Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.cast_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.find.congr_simp Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add inv_mul_cancel₀ mul_inv_cancel₀ eq_of_sub_eq_zero Algebra.to_smulCommClass LinearMap.mulLeft_apply IsScalarTower.right LinearMap.mulRight_apply Function.iterate_succ_apply' one_mul mul_assoc mul_one mul_sub_left_distrib inv_mul_cancel_of_invertible mul_sub exists_pow_mem_center_of_inseparable one_ne_zero NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd IsMulCentral.comm GroupWithZero.conj_pow₀ one_pow add_pow_expChar_pow_of_commute Commute.one_left sub_eq_iff_eq_add
exists_separable_and_not_isCentral' 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing	—	le_bot_iff Algebra.IsCentral.out Eq.trans_ne Subalgebra.toSubring_injective IsSimpleRing.instNontrivial DivisionRing.isSimpleRing IsScalarTower.of_algebraMap_eq IsScalarTower.algebraMap_apply RingEquiv.apply_symm_apply Algebra.IsAlgebraic.tower_top exists_separable_and_not_isCentral Subalgebra.center_toSubring IsSeparable.tower_top

---

← Back to Index