Commit 2024-07-09 09:58 6ce9f7a0

View on Github →

chore: Split RingTheory.Trace and RingTheory.Norm (#14446) We split RingTheory.Trace in RingTheory.Trace.Defs and RingTheory.Trace.Basic. Similarly for RingTheory.Norm.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Finite/Trace.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/LinearAlgebra/FreeModule/Norm.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/RingTheory/Complex.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/Localization/NormTrace.lean

Renamed Mathlib/RingTheory/Norm.lean to Mathlib/RingTheory/Norm/Basic.lean

deleted theorem Algebra.norm_algebraMap_of_basis

deleted theorem Algebra.norm_apply

deleted theorem Algebra.norm_eq_matrix_det

deleted theorem Algebra.norm_eq_one_of_not_exists_basis

deleted theorem Algebra.norm_eq_one_of_not_module_finite

Created Mathlib/RingTheory/Norm/Defs.lean

added theorem Algebra.norm_algebraMap_of_basis

added theorem Algebra.norm_apply

added theorem Algebra.norm_eq_matrix_det

added theorem Algebra.norm_eq_one_of_not_exists_basis

added theorem Algebra.norm_eq_one_of_not_module_finite

Modified Mathlib/RingTheory/NormTrace.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Renamed Mathlib/RingTheory/Trace.lean to Mathlib/RingTheory/Trace/Basic.lean

deleted theorem Algebra.traceForm_apply

deleted theorem Algebra.traceForm_isSymm

deleted theorem Algebra.traceForm_toMatrix

modified theorem Algebra.traceForm_toMatrix_powerBasis

deleted theorem Algebra.trace_algebraMap

deleted theorem Algebra.trace_algebraMap_of_basis

deleted theorem Algebra.trace_apply

deleted theorem Algebra.trace_comp_trace

deleted theorem Algebra.trace_comp_trace_of_basis

deleted theorem Algebra.trace_eq_matrix_trace

deleted theorem Algebra.trace_eq_zero_of_not_exists_basis

deleted theorem Algebra.trace_prod

deleted theorem Algebra.trace_prod_apply

deleted theorem Algebra.trace_trace

deleted theorem Algebra.trace_trace_of_basis

Created Mathlib/RingTheory/Trace/Defs.lean

added theorem Algebra.traceForm_apply

added theorem Algebra.traceForm_isSymm

added theorem Algebra.traceForm_toMatrix

added theorem Algebra.trace_algebraMap

added theorem Algebra.trace_algebraMap_of_basis

added theorem Algebra.trace_apply

added theorem Algebra.trace_comp_trace

added theorem Algebra.trace_comp_trace_of_basis

added theorem Algebra.trace_eq_matrix_trace

added theorem Algebra.trace_eq_zero_of_not_exists_basis

added theorem Algebra.trace_prod

added theorem Algebra.trace_prod_apply

added theorem Algebra.trace_trace

added theorem Algebra.trace_trace_of_basis