leanprover-community/mathlib

Pull Requests Commits

Define `fin.cycle_range` in terms of a new `fin.cycle_all`

Vierkantor committed 4 years ago

0107630b

Vierkantor committed 4 years ago

8f746be2

Generalize `sign_cycle_range`

Vierkantor committed 4 years ago

4318e1bd

Define `cycle_range_of_apply`

Vierkantor committed 4 years ago

7b5575d5

feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))`

Vierkantor committed 4 years ago

8c89ff7a

chore(scripts): update nolints.txt (#6763)

leanprover-community-bot committed 4 years ago

a1305bea

ci(*): lint 'Authors: ' line (#6750)

kim-em committed 4 years ago

cc11e44c

feat(data/equiv/local_equiv): define `piecewise` and `disjoint_union` (#6700)

urkud committed 4 years ago

c3e40bef

doc(field_theory/normal): Add authors (#6759)

tb65536 committed 4 years ago

02f77ab9

chore(algebra/char_p/basic): weaken assumptions integral_domain --> semiring+ (#6753)

adomani committed 4 years ago

aea7dfbc

feat(normed_space/inner_product): euclidean_space.norm_eq (#6744)

pechersky committed 4 years ago

a10bc3d3

chore(*): update `injective` lemma names to match the naming guide (#6740)

eric-wieser committed 4 years ago

e1ff2dff

feat(ring_theory/polynomial): the symmetric and homogenous polynomials form a subalgebra and submodules, respectively (#6666)

eric-wieser committed 4 years ago

83b0981b

refactor(category_theory/limits): split file (#6751)

kim-em committed 4 years ago

744d59af

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

kim-em committed 4 years ago

58581d0f

refactor(algebra/algebra/basic): change submodule.restrict_scalars to use is_scalar_tower (#6745)

eric-wieser committed 4 years ago

542ff6af

feat(algebra/associated): Primes that divide each other are associated (#6732)

thejohncrafter committed 4 years ago

59cda3bb

feat(ring_theory/principal_ideal_domain): The generator of a principal prime ideal is a prime (#6731)

thejohncrafter committed 4 years ago

db2a972d

feat(data/padics/padic_norm): p-adic norm of primes other than p (#6730)

thejohncrafter committed 4 years ago

b4afd642

feat(group_theory/quaternion_group): define the (generalised) quaternion groups (#6683)

Julian-Kuelshammer committed 4 years ago

216aecd7

doc(category_theory): convert comments about universes to library note (#6748)

kim-em committed 4 years ago

8116851f

chore(scripts): update nolints.txt (#6747)

leanprover-community-bot committed 4 years ago

e955a6bd

feat(ring_theory/finiteness): add transitivity of finite presentation (#6640)

riccardobrasca committed 4 years ago

9b8d41a3

chore(data/mv_polynomial/basic): add coeff_smul to match coeff_add etc (#6742)

eric-wieser committed 4 years ago

804b0ede

feat(ring_theory/roots_of_unity): Restrict ring homomorphism to roots of unity (#6646)

tb65536 committed 4 years ago

30b34552

chore(category_theory/limits/creates): fix typo in docstring (#6738)

b-mehta committed 4 years ago

9507a34f

chore(combinatorics/simple_graph): remove bad simp attribute (#6736)

b-mehta committed 4 years ago

6e1143ab

refactor(data/multiset/basic): consistently use 'nsmul' in names (#6735)

Ruben-VandeVelde committed 4 years ago

ce8a6ca0

feat(algebra/module/submodule): add `smul_of_tower_mem` (#6712)

eric-wieser committed 4 years ago

7e82bba0

feat(bounded_continuous_function): transport structure to C(α, β) when α compact (#6701)

kim-em committed 4 years ago

4ae81c2f

Older