[Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic #22843

ScottCarnahan · 2025-03-11T17:34:15Z

This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map.

github-actions · 2025-03-11T17:35:17Z

PR summary 4d48848479

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Splits.mem_subfield_of_isRoot
+ Subfield.card_bot
+ Subfield.fintypeBot
+ Subfield.mem_bot_iff_pow_eq_self
+ Subfield.roots_X_pow_char_sub_X_bot
+ Subfield.splits_bot
+ fieldRange_castHom_eq_bot
+ instance : Subsingleton (Subfield (ZMod p))
+ mem_bot_iff_intCast
+ rangeRestrictField_bijective

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

jcommelin

Thanks 🎉

bors merge

alreadydone

I'm not sure why computing the Galois group of finite fields needs this PR; at least the canonical generator of Gal(L/K) can be defined without mentioning the prime subfield. I'm now trying to do a quick proof without the Fintype.card->Nat.card refactor.

Mathlib/FieldTheory/Finite/Basic.lean

Mathlib/Algebra/Field/Subfield/Basic.lean

Mathlib/FieldTheory/Finite/Basic.lean

…sitive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map.

jcommelin · 2025-03-12T13:43:53Z

bors r-

mathlib-bors · 2025-03-12T13:43:55Z

Canceled.

pechersky

Thanks for factoring out the Nat proofs. The neg pow lemma is true in general over odd p, not just for rings with char p; the p=2 is the charP special case. But I don't think you need to generalize it further. LGTM

alreadydone

Will continue after lunch :)

Mathlib/Algebra/Field/Subfield/Basic.lean

Mathlib/FieldTheory/Finite/Basic.lean

Mathlib/Algebra/Field/Subfield/Basic.lean

Mathlib/FieldTheory/Finite/Basic.lean

alreadydone

These are my last comments, and I've put additional golfs / suggestions of renames in this commit.

Mathlib/FieldTheory/Finite/Basic.lean

alreadydone

Thank you!
maintainer merge

github-actions · 2025-03-15T00:10:19Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

riccardobrasca · 2025-03-15T13:01:54Z

Thanks!

bors merge

…sitive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map.

mathlib-bors · 2025-03-15T13:49:11Z

Pull request successfully merged into master.

Build succeeded:

…vProdLpPiLp` (#22993) * feat: scalar tower instances for quotients (#22951) We already have the `SMulCommClass` and `IsScalarTower` versions for `RingQuot`; this develops them for `Con` and `RingCon`, with the eventual aim of replacing `RingQuot` with `RingCon.Quotient`. * chore(Order/Group/Abs): use `@[to_additive]` (#22468) * feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map. * docs(Data/Real/EReal): fix capitalization error (#22943) Changes `Ereal` to `EReal` in the module docstring for `Data/Real/EReal`. * chore(Ideal/Quotient): change `Fintype` to `Finite` (#22947) As discussed [here](#22902 (comment)) * feat: add `norm_num` extensions for factorials (#8832) Add `norm_num` extensions to evaluate `Nat.factorial`, `Nat.ascFactorial` and `Nat.descFactorial`. Co-authored-by: Eric Wieser <[email protected]> * perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968) This PR is in the same spirit as #22953. The problem is that some instances about category theoretical limits have silly side conditions that end up searching through the whole algebraic type class hierarchy. This PR attempts to keep the type class search limited to category theoretical type classes. * feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940) * feat: API for continuous extension of meromorphic functions (#22867) Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. * feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945) cos 1 is approximately 0.5403..., so this bound is fairly tight. Co-authored-by: Vlad Tsyrklevich <[email protected]> * chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935) This better matches the naming convention. * working on it. * Added sup_disjSum and inf_disjSum. * Finished one branch. * Finished proof. --------- Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> Co-authored-by: Scott Carnahan <[email protected]> Co-authored-by: plp127 <[email protected]> Co-authored-by: Xavier Roblot <[email protected]> Co-authored-by: Sebastian Zimmer <[email protected]> Co-authored-by: JovanGerb <[email protected]> Co-authored-by: Stefan Kebekus <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

add lemmas

9e12f26

ScottCarnahan added the t-algebra Algebra (groups, rings, fields, etc) label Mar 11, 2025

jcommelin changed the title ~~feat (FieldTheory/Finite/Basic): Lemmas about the prime subfield in positive characteristic.~~ feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic Mar 12, 2025

jcommelin reviewed Mar 12, 2025

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Mar 12, 2025

alreadydone reviewed Mar 12, 2025

View reviewed changes

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

pechersky reviewed Mar 12, 2025

View reviewed changes

Mathlib/Algebra/Field/Subfield/Basic.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot removed the ready-to-merge This PR has been sent to bors. label Mar 12, 2025

ScottCarnahan added 4 commits March 13, 2025 07:49

Merge branch 'master' into ScottCarnahan/bot

687dd99

follow reviewers' suggestions

d29915f

oops forgot about the name change

2b5574d

rm bad simp

1ea72e4

jcommelin requested review from alreadydone and pechersky March 13, 2025 05:28

add better simp lemma

fc464a0

pechersky approved these changes Mar 13, 2025

View reviewed changes

alreadydone reviewed Mar 14, 2025

View reviewed changes

Merge branch 'master' into ScottCarnahan/bot

0a7b44a

alreadydone reviewed Mar 14, 2025

View reviewed changes

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/Finite/Basic.lean Outdated Show resolved Hide resolved

follow reviewer's suggestions

4d48848

alreadydone approved these changes Mar 15, 2025

View reviewed changes

github-actions bot added the maintainer-merge label Mar 15, 2025

leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge labels Mar 15, 2025

mathlib-bors bot changed the title ~~feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic~~ [Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic Mar 15, 2025

mathlib-bors bot closed this Mar 15, 2025

mathlib-bors bot deleted the ScottCarnahan/bot branch March 15, 2025 13:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic #22843

[Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic #22843

ScottCarnahan commented Mar 11, 2025

github-actions bot commented Mar 11, 2025 •

edited

Loading

Declarations diff

jcommelin left a comment

alreadydone left a comment

jcommelin commented Mar 12, 2025

mathlib-bors bot commented Mar 12, 2025

pechersky left a comment •

edited

Loading

alreadydone left a comment

alreadydone left a comment

alreadydone left a comment

github-actions bot commented Mar 15, 2025

riccardobrasca commented Mar 15, 2025

mathlib-bors bot commented Mar 15, 2025

[Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic #22843

[Merged by Bors] - feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic #22843

Conversation

ScottCarnahan commented Mar 11, 2025

github-actions bot commented Mar 11, 2025 • edited Loading

PR summary 4d48848479

Import changes for modified files

Declarations diff

jcommelin left a comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

jcommelin commented Mar 12, 2025

mathlib-bors bot commented Mar 12, 2025

pechersky left a comment • edited Loading

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

github-actions bot commented Mar 15, 2025

riccardobrasca commented Mar 15, 2025

mathlib-bors bot commented Mar 15, 2025

github-actions bot commented Mar 11, 2025 •

edited

Loading

pechersky left a comment •

edited

Loading