Commits leanprover-community/mathlib

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

eric-wieser committed 5 years ago

542ff6af

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

thejohncrafter committed 5 years ago

59cda3bb

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

thejohncrafter committed 5 years ago

db2a972d

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

thejohncrafter committed 5 years ago

b4afd642

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

Julian-Kuelshammer committed 5 years ago

216aecd7

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

kim-em committed 5 years ago

8116851f

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

leanprover-community-bot committed 5 years ago

e955a6bd

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

riccardobrasca committed 5 years ago

9b8d41a3

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

eric-wieser committed 5 years ago

804b0ede

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

tb65536 committed 5 years ago

30b34552

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

b-mehta committed 5 years ago

9507a34f

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

b-mehta committed 5 years ago

6e1143ab

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

Ruben-VandeVelde committed 5 years ago

ce8a6ca0

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

eric-wieser committed 5 years ago

7e82bba0

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

kim-em committed 5 years ago

4ae81c2f

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

eric-wieser committed 5 years ago

0b0fd528

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

paulvanwamelen committed 5 years ago

6db70c98

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

RemyDegenne committed 5 years ago

41191815

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

mo271 committed 5 years ago

fb28eac0

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

jcommelin committed 5 years ago

83a4b8b9

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

Ruben-VandeVelde committed 5 years ago

73922b54

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

apnelson1 committed 5 years ago

1f50530a

feat(ring_theory/algebraic data/real/irrational): add a proof that a transcendental real number is irrational (#6721)

adomani committed 5 years ago

13453191

chore(linear_algebra/determinant): redefine det using multilinear_map.alternatization (#6708)

eric-wieser committed 5 years ago

4b1d5886

feat(ring_theory/polynomial): Pochhammer polynomials (#6598)

kim-em committed 5 years ago

84933f12

feat(field_theory/normal): Tower of solvable extensions is solvable (#6643)

tb65536 committed 5 years ago

861f5946

refactor(group_theory/order_of_element): now makes sense for infinite monoids (#6587)

Julian-Kuelshammer committed 5 years ago

6f6b548b

feat(tactic/norm_num): support for nat.cast + int constructors (#6235)

digama0 committed 5 years ago

3e7a56ee

refactor(topology/metric_space/basic): add pseudo_metric (#6716)

riccardobrasca committed 5 years ago

d292fd7e

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

leanprover-community-bot committed 5 years ago

3936f5fd