Commit 2024-04-23 14:29 bdfbc7fa

View on Github →

chore: split RingTheory.Nilpotent (#12184) Mathlib.RingTheory.Nilpotent has a few very simple definitions (Mathlib.Data.Nat.Lattice is sufficient to state them), but needs some pretty heavy imports (ideals, linear algebra) towards the end. This change moves the heavier parts into a new file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/Reduced.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/Dynamics/Newton.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/LocalProperties.lean

Deleted Mathlib/RingTheory/Nilpotent.lean

deleted theorem Commute.add_pow_add_eq_zero_of_pow_eq_zero

deleted theorem Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero

deleted theorem Commute.isNilpotent_add

deleted theorem Commute.isNilpotent_mul_left

deleted theorem Commute.isNilpotent_mul_right

deleted theorem Commute.isNilpotent_sub

deleted theorem IsNilpotent.eq_zero

deleted theorem IsNilpotent.isUnit_add_left_of_commute

deleted theorem IsNilpotent.isUnit_add_one

deleted theorem IsNilpotent.isUnit_add_right_of_commute

deleted theorem IsNilpotent.isUnit_one_add

deleted theorem IsNilpotent.isUnit_one_sub

deleted theorem IsNilpotent.isUnit_sub_one

deleted theorem IsNilpotent.map

deleted theorem IsNilpotent.map_iff

deleted theorem IsNilpotent.mk

deleted theorem IsNilpotent.neg

deleted theorem IsNilpotent.of_pow

deleted theorem IsNilpotent.pow_iff_pos

deleted theorem IsNilpotent.pow_of_pos

deleted theorem IsNilpotent.pow_succ

deleted theorem IsNilpotent.smul

deleted theorem IsNilpotent.zero

deleted def IsNilpotent

deleted theorem IsRadical.of_dvd

deleted def IsRadical

deleted theorem IsUnit.isNilpotent_mul_unit_of_commute_iff

deleted theorem IsUnit.isNilpotent_unit_mul_of_commute_iff

deleted theorem LinearMap.isNilpotent_mulLeft_iff

deleted theorem LinearMap.isNilpotent_mulRight_iff

deleted theorem LinearMap.isNilpotent_toMatrix_iff

deleted theorem Module.End.IsNilpotent.mapQ

deleted theorem NoZeroSMulDivisors.isReduced

deleted theorem Prime.isRadical

deleted theorem RingHom.ker_isRadical_iff_reduced_of_surjective

deleted theorem eq_zero_of_nilpotencyClass_eq_one

deleted theorem isNilpotent_iff_eq_zero

deleted theorem isNilpotent_neg_iff

deleted theorem isNilpotent_of_pos_nilpotencyClass

deleted theorem isNilpotent_of_subsingleton

deleted theorem isNilpotent_sum

deleted theorem isRadical_iff_pow_one_lt

deleted theorem isRadical_iff_span_singleton

deleted theorem isReduced_iff_pow_one_lt

deleted theorem isReduced_of_injective

deleted theorem mem_nilradical

deleted theorem nilpotencyClass_eq_one

deleted theorem nilpotencyClass_eq_succ_iff

deleted theorem nilpotencyClass_eq_zero_of_subsingleton

deleted theorem nilpotencyClass_zero

deleted theorem nilpotent_iff_mem_prime

deleted def nilradical

deleted theorem nilradical_eq_sInf

deleted theorem nilradical_eq_zero

deleted theorem nilradical_le_prime

deleted theorem not_isNilpotent_one

deleted theorem pos_nilpotencyClass_iff

deleted theorem pow_nilpotencyClass

deleted theorem pow_pred_nilpotencyClass

deleted theorem zero_isRadical_iff

Created Mathlib/RingTheory/Nilpotent/Basic.lean

added theorem Commute.add_pow_add_eq_zero_of_pow_eq_zero

added theorem Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero

added theorem Commute.isNilpotent_add

added theorem Commute.isNilpotent_sub

added theorem IsNilpotent.isUnit_add_left_of_commute

added theorem IsNilpotent.isUnit_add_one

added theorem IsNilpotent.isUnit_add_right_of_commute

added theorem IsNilpotent.isUnit_one_add

added theorem IsNilpotent.isUnit_one_sub

added theorem IsNilpotent.isUnit_sub_one

added theorem IsNilpotent.neg

added theorem IsNilpotent.smul

added theorem IsRadical.of_dvd

added theorem NoZeroSMulDivisors.isReduced

added theorem Prime.isRadical

added theorem isNilpotent_neg_iff

added theorem isNilpotent_sum

added theorem isReduced_iff_pow_one_lt

added theorem zero_isRadical_iff

Created Mathlib/RingTheory/Nilpotent/Defs.lean

added theorem Commute.isNilpotent_mul_left

added theorem Commute.isNilpotent_mul_right

added theorem IsNilpotent.eq_zero

added theorem IsNilpotent.map

added theorem IsNilpotent.map_iff

added theorem IsNilpotent.mk

added theorem IsNilpotent.of_pow

added theorem IsNilpotent.pow_iff_pos

added theorem IsNilpotent.pow_of_pos

added theorem IsNilpotent.pow_succ

added theorem IsNilpotent.zero

added def IsNilpotent

added def IsRadical

added theorem IsUnit.isNilpotent_mul_unit_of_commute_iff

added theorem IsUnit.isNilpotent_unit_mul_of_commute_iff

added theorem eq_zero_of_nilpotencyClass_eq_one

added theorem isNilpotent_iff_eq_zero

added theorem isNilpotent_of_pos_nilpotencyClass

added theorem isNilpotent_of_subsingleton

added theorem isRadical_iff_pow_one_lt

added theorem isReduced_of_injective

added theorem nilpotencyClass_eq_one

added theorem nilpotencyClass_eq_succ_iff

added theorem nilpotencyClass_eq_zero_of_subsingleton

added theorem nilpotencyClass_zero

added theorem not_isNilpotent_one

added theorem pos_nilpotencyClass_iff

added theorem pow_nilpotencyClass

added theorem pow_pred_nilpotencyClass

Created Mathlib/RingTheory/Nilpotent/Lemmas.lean

added theorem LinearMap.isNilpotent_mulLeft_iff

added theorem LinearMap.isNilpotent_mulRight_iff

added theorem LinearMap.isNilpotent_toMatrix_iff

added theorem Module.End.IsNilpotent.mapQ

added theorem RingHom.ker_isRadical_iff_reduced_of_surjective

added theorem isRadical_iff_span_singleton

added theorem mem_nilradical

added theorem nilpotent_iff_mem_prime

added def nilradical

added theorem nilradical_eq_sInf

added theorem nilradical_eq_zero

added theorem nilradical_le_prime

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/RingTheory/QuotientNilpotent.lean