Commits

Branch selector

 master

User selector

acmepjz

All time

Commit History

Commits on Feb 23, 2024

• feat(FieldTheory/Adjoin): add IntermediateField.[fin]rank_bot' (leanprover-community#10896)

  acmepjz

  committedFeb 23, 2024
  c951d81

• feat(Algebra/Associated): add Associated.map (leanprover-community#10895)

  acmepjz

  committedFeb 23, 2024
  0fb7df8

• feat(FieldTheory/Separable): add result on Associated and Polynomial.Separable (leanprover-community#10897)

  acmepjz

  committedFeb 23, 2024
  11b3632

Commits on Feb 22, 2024

• feat(Algebra/CharP/IntermediateField): characteristic of intermediate fields (leanprover-community#10839)

  acmepjz

  committedFeb 22, 2024
  965479b

Commits on Feb 15, 2024

• feat(Algebra/CharP/*): add RingHom.(charP|expChar)[_iff] (leanprover-community#10574)

  acmepjz

  committedFeb 15, 2024
  4b36afc

• feat(FieldTheory/Perfect): add roots_X_pow_char[_pow]_sub_C[_pow] (leanprover-community#10573)

  acmepjz

  committedFeb 15, 2024
  9e9d545

• feat: add some simple results regarding polynomials (leanprover-community#10572)

  acmepjz

  committedFeb 15, 2024
  f23db5a

• feat: add Multiset.toFinset_(eq_singleton|card_eq_one)_iff (leanprover-community#10571)

  acmepjz

  committedFeb 15, 2024
  51f0486

Commits on Feb 14, 2024

• feat(FieldTheory/Perfect): add various convenient lemmas for iterateFrobenius[Equiv] (leanprover-community#10405)

  acmepjz

  committedFeb 14, 2024
  3809ca5

Commits on Feb 13, 2024

• feat: Add Finset.card_union_eq_card_add_card and golf (leanprover-community#10471)

  

  acmepjz

  and

  YaelDillies

  committedFeb 13, 2024
  1115238

Commits on Feb 6, 2024

• refactor(FieldTheory/PerfectClosure): change the order of some results (leanprover-community#10282)

  acmepjz

  committedFeb 6, 2024
  ec4beba

• feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions (leanprover-community#9488)

  

  acmepjz

  and

  alreadydone

  committedFeb 6, 2024
  d172b39

Commits on Feb 2, 2024

• feat(RingTheory/Polynomial/IrreducibleRing): add Monic.irreducible_of_irreducible_map_of_isPrime_nilradical (leanprover-community#10157)

  acmepjz

  committedFeb 2, 2024
  382799b

Commits on Jan 19, 2024

• feat({Ring|Field}Theory/Adjoin): add various results on adjoin (leanprover-community#9790)

  

  acmepjz

  and

  alreadydone

  committedJan 19, 2024
  50388bc

• feat(FieldTheory/IsAlgClosed/Basic): add IsAlgClosed.perfectField instance (leanprover-community#9710)

  

  acmepjz

  and

  alreadydone

  committedJan 19, 2024
  d0f6060

• feat(LinearAlgebra/LinearIndependent): add linearIndependent_iff_finset_linearIndependent (leanprover-community#9797)

  acmepjz

  committedJan 19, 2024
  4bb560b

Commits on Jan 18, 2024

• feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow (leanprover-community#9799)

  acmepjz

  committedJan 18, 2024
  1e74fcf

Commits on Jan 15, 2024

• feat: add equivMap[OfInjective] for subalgebra and intermediate field (leanprover-community#9709)

  acmepjz

  committedJan 15, 2024
  6e66ddc

Commits on Jan 10, 2024

• feat(Algebra/CharP/ExpChar): add more results for ExpChar parallel to CharP (leanprover-community#9573)

  acmepjz

  committedJan 10, 2024
  fd4eb93

Commits on Jan 8, 2024

• feat(FieldTheory/Adjoin): add exists_finset_of_mem_adjoin (leanprover-community#9524)

  acmepjz

  committedJan 8, 2024
  ca1a92f

• feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field (leanprover-community#9522)

  acmepjz

  committedJan 8, 2024
  417f344

• doc(FieldTheory/IsAlgClosed/Basic): add a TODO (leanprover-community#9519)

  acmepjz

  committedJan 8, 2024
  70edc53

• chore(FieldTheory/SeparableDegree): add Separable.natSepDegree_eq_natDegree and golf (leanprover-community#9525)

  acmepjz

  committedJan 8, 2024
  1de7e66

Commits on Jan 1, 2024

• feat(FieldTheory/SeparableClosure): (relative) separable closure (leanprover-community#9338)

  acmepjz

  committedJan 1, 2024
  bded32a

Commits on Dec 28, 2023

• doc(FieldTheory/SeparableDegree): fix the formula in docstring (leanprover-community#9318)

  acmepjz

  committedDec 28, 2023
  288b6c5

• feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials (leanprover-community#9041)

  

  acmepjz

  and

  jcommelin

  committedDec 28, 2023
  8788d9a

Commits on Dec 26, 2023

• feat(FieldTheory/Perfect): add rootsExpand[Pow]EquivRoots[_apply] (leanprover-community#9271)

  acmepjz

  committedDec 26, 2023
  2041984

• chore(RingTheory/Polynomial/SeparableDegree): add HasSeparableContraction.isSeparableContraction and ... (leanprover-community#9272)

  acmepjz

  committedDec 26, 2023
  caeafef

Commits on Dec 25, 2023

• feat(Data/Polynomial/Expand): add leadingCoeff_expand and monic_expand_iff (leanprover-community#9261)

  acmepjz

  committedDec 25, 2023
  b1556bb

• feat(Algebra/CharP/ExpChar): add expChar[_pow]_pos (leanprover-community#9260)

  acmepjz

  committedDec 25, 2023
  5ca2c4b

• feat(FieldTheory/Adjoin): add exists_lt_finrank_of_infinite_dimensional (leanprover-community#9262)

  acmepjz

  committedDec 25, 2023
  f1addf8

• feat(FieldTheory/Separable): add some results regarding separable and no repeated roots (leanprover-community#9263)

  acmepjz

  committedDec 25, 2023
  490c92f

Commits on Dec 22, 2023

• feat(LinearAlgebra/Dimension): add various surjective_injective results (leanprover-community#9156)

  acmepjz

  committedDec 22, 2023
  98067b2

Commits on Dec 18, 2023

• feat(Mathlib/FieldTheory/Separable): add Polynomial.Separable.isIntegral and golf (leanprover-community#9134)

  acmepjz

  committedDec 18, 2023
  f94379b

Commits on Dec 14, 2023

• feat(Algebra/CharP/ExpChar): add some results parallel to CharP (leanprover-community#8860)

  acmepjz

  committedDec 14, 2023
  1d5e93a

Pagination

PreviousNext