Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit history

Commits on Dec 3, 2021

• chore(*): protect `to_fun` and `map_{add,zero,mul,one,div}` (#10580)

  Show description for 8bb26a7
  Vierkantor

  committed
  8bb26a7

  Copy full SHA for 8bb26a7

Commits on Nov 29, 2021

• chore(*): cleanup unneeded uses of by_cases across the library (#10523)

  Show description for bc4ed5c
  alexjbest

  committed
  bc4ed5c

  Copy full SHA for bc4ed5c

Commits on Nov 23, 2021

• refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347)

  Show description for ca7347c
  eric-wieser

  committed
  ca7347c

  Copy full SHA for ca7347c

Commits on Nov 17, 2021

• lint(*): curly braces linter (#10280)

  Show description for 8f6fd1b
  jcommelin

  committed
  8f6fd1b

  Copy full SHA for 8f6fd1b

Commits on Oct 31, 2021

• chore(*): clean up the library using to_additive (#9790)

  Show description for b7f120f
  alexjbest

  committed
  b7f120f

  Copy full SHA for b7f120f

Commits on Oct 27, 2021

• refactor(*): rename fpow and gpow to zpow (#9989)

  Show description for c529711
  sgouezel

  committed
  c529711

  Copy full SHA for c529711

Commits on Sep 23, 2021

• refactor(group_theory/subgroup,linear_algebra/basic): put pointwise actions in their own files to match submonoid (#9312)

  eric-wieser

  committed
  671b179

  Copy full SHA for 671b179

Commits on Aug 21, 2021

• chore(*): remove spurious whitespace (#8769)

  sgouezel

  committed
  f36c98e

  Copy full SHA for f36c98e

Commits on Aug 1, 2021

• chore(deprecated/*): Make deprecated classes into structures (#8178)

  Show description for f961b28
  kbuzzard

  committed
  f961b28

  Copy full SHA for f961b28

Commits on Jul 27, 2021

• feat(data/nat/totient): totient_mul (#8441)

  Show description for 1b0391a
  ChrisHughes24

  committed
  1b0391a

  Copy full SHA for 1b0391a

Commits on Jun 7, 2021

• feat(algebra/ring/basic): define non-unital, non-associative rings (#6786)

  Show description for ef7aa94
  

  4 peoplecommitted
  ef7aa94

  Copy full SHA for ef7aa94

Commits on May 10, 2021

• chore(deprecated/group): relax monoid to mul_one_class (#7556)

  Show description for 3417ee0
  eric-wieser

  committed
  3417ee0

  Copy full SHA for 3417ee0

Commits on Apr 25, 2021

• refactor(*): kill int multiplication diamonds (#7255)

  Show description for 8e4ef23
  

  4 peoplecommitted
  8e4ef23

  Copy full SHA for 8e4ef23

Commits on Apr 14, 2021

• refactor(*): kill nat multiplication diamonds (#7084)

  Show description for 6380155
  

  sgouezel

  and

  kim-em

  committed
  6380155

  Copy full SHA for 6380155

Commits on Apr 6, 2021

• feat(algebra/group/conj): `is_conj` for `monoid`s, `is_conj.setoid`, and `conj_classes` (#6896)

  Show description for 5f0dbf6
  

  awainverse

  and

  jcommelin

  committed
  5f0dbf6

  Copy full SHA for 5f0dbf6

Commits on Mar 31, 2021

• refactor(algebra/*): add new `mul_one_class` and `add_zero_class` for non-associative monoids (#6865)

  Show description for 5f1b450
  eric-wieser

  committed
  5f1b450

  Copy full SHA for 5f1b450

Commits on Mar 29, 2021

• feat(group_theory/{subgroup, order_of_element}): refactors simple groups, classifies finite simple abelian/solvable groups (#6926)

  Show description for 87bc893
  awainverse

  committed
  87bc893

  Copy full SHA for 87bc893

Commits on Mar 26, 2021

• refactor(algebra/field): allow custom `div` (#6874)

  urkud

  committed
  c658f5c

  Copy full SHA for c658f5c

Commits on Mar 18, 2021

• chore(*): normalize Authors: line (#6749)

  Show description for 58581d0
  kim-em

  committed
  58581d0

  Copy full SHA for 58581d0

Commits on Feb 27, 2021

• chore(*): split lines and move module doc `measure_theory/category/Meas` (#6459)

  Julian-Kuelshammer

  committed
  aa0b274

  Copy full SHA for aa0b274

Commits on Feb 14, 2021

• chore(algebra/group/basic): remove three redundant lemmas (#6197)

  Show description for 22b26d3
  Julian-Kuelshammer

  committed
  22b26d3

  Copy full SHA for 22b26d3

Commits on Feb 1, 2021

• chore(*): split some long lines (#5997)

  urkud

  committed
  684f4f5

  Copy full SHA for 684f4f5

Commits on Jan 9, 2021

• chore(algebra/group/hom): fix additive version of docstring (#5660)

  jcommelin

  committed
  0cd70d0

  Copy full SHA for 0cd70d0

Commits on Dec 16, 2020

• chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303)

  Show description for 1221ab6
  Vierkantor

  committed
  1221ab6

  Copy full SHA for 1221ab6

Commits on Dec 11, 2020

• chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302)

  Show description for a372dfc
  

  Vierkantor

  and

  sgouezel

  committed
  a372dfc

  Copy full SHA for a372dfc

Commits on Nov 22, 2020

• chore(logic/basic): add `forall_apply_eq_imp_iff₂` (#5072)

  Show description for 87439b9
  urkud

  committed
  87439b9

  Copy full SHA for 87439b9

Commits on Nov 17, 2020

• feat(algebra/group_with_zero): Bundled `monoid_with_zero_hom` (#4995)

  Show description for 86b0971
  eric-wieser

  committed
  86b0971

  Copy full SHA for 86b0971

Commits on Nov 12, 2020

• chore(deprecated/group): Do not import `deprecated` from `equiv/mul_add` (#4989)

  Show description for 6e64df5
  eric-wieser

  committed
  6e64df5

  Copy full SHA for 6e64df5

Commits on Nov 11, 2020

• doc(type_classes): Explain the use of {} instance arguments (#4976)

  Show description for d4aabf9
  eric-wieser

  committed
  d4aabf9

  Copy full SHA for d4aabf9

Commits on Oct 23, 2020

• fix(deprecated/group): Correct the name of `is_add_group_hom has_neg.neg` (#4755)

  Show description for 0bbf3e2
  eric-wieser

  committed
  0bbf3e2

  Copy full SHA for 0bbf3e2

• fix(deprecated/*): remove instances (#4735)

  Show description for fb4aee0
  

  jcommelin

  and

  gebner

  committed
  fb4aee0

  Copy full SHA for fb4aee0

Commits on Oct 13, 2020

• fix(big_operators): fix imports (#4588)

  Show description for 766d860
  fpvandoorn

  committed
  766d860

  Copy full SHA for 766d860

Commits on Sep 26, 2020

• feat(field_theory): prove primitive element theorem (#4153)

  Show description for 253b120
  

  tb65536

  and

  pglutz

  committed
  253b120

  Copy full SHA for 253b120

Commits on Sep 17, 2020

• refactor(field-theory/subfield): bundled subfields (#4159)

  Show description for 5a2e7d7
  Vierkantor

  committed
  5a2e7d7

  Copy full SHA for 5a2e7d7

Commits on Sep 9, 2020

• chore(*): use new `extends_priority` default of 100 (#4066)

  Show description for 2ab31f9
  rwbarton

  committed
  2ab31f9

  Copy full SHA for 2ab31f9