Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 19:11 e6f4852b

View on Github →

feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g (#10767) Precursor to #10692.

Estimated changes

Modified src/data/nat/lattice.lean

added theorem set.infinite.nat.Sup_eq_zero

Modified src/group_theory/exponent.lean

modified theorem monoid.exponent_dvd_of_forall_pow_eq_one

added theorem monoid.exponent_eq_max'_order_of

added theorem monoid.exponent_eq_supr_order_of'

added theorem monoid.exponent_eq_supr_order_of

added theorem monoid.exponent_eq_zero_iff

added theorem monoid.exponent_eq_zero_iff_range_order_of_infinite

added theorem monoid.exponent_eq_zero_of_order_zero

added theorem monoid.exponent_ne_zero_iff_range_order_of_finite

added theorem monoid.exponent_ne_zero_of_fintype

modified theorem monoid.lcm_order_eq_exponent

modified theorem monoid.lcm_order_of_dvd_exponent

added theorem nat.prime.exists_order_of_eq_pow_padic_val_nat_exponent