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 DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Nat.iterate DFunLike.coe Module.End 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 Ring.toNonAssocRing	—	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 DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Monoid.toNatPow 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 DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center	Monoid.toNatPow 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 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