leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

537f29c0

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

chore(analysis/normed_space/extend): provide a version without restrict_scalars (#6693)

eric-wieser committed 4 years ago

0b0fd528

refactor(linear_algebra/determinant): refactor proof of upper_two_block_triangular_det (#6690)

paulvanwamelen committed 4 years ago

6db70c98

feat(measure_theory/l2_space): L2 is an inner product space (#6596)

RemyDegenne committed 4 years ago

41191815

feat(number_theory/bernoulli): Faulhaber's theorem (#6409)

mo271 committed 4 years ago

fb28eac0

chore(group_theory/subgroup): fix typo in docstring (#6722)

jcommelin committed 4 years ago

83a4b8b9

feat(data/zsqrtd/basic): add some lemmas about conj, norm (#6715)

Ruben-VandeVelde committed 4 years ago

73922b54

feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629)

apnelson1 committed 4 years ago

1f50530a

Older