Commit 2025-03-11 07:07 fa9f8699

View on Github →

chore: review of erw in NumberTheory/ (#22813)

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom/Rat.lean

added theorem RingHom.toRatAlgHom_apply

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean