leanprover-community/mathlib3

Pull Requests Commits

feat(data/real/nnreal): ℝ is an ℝ≥0-algebra (#6560)

adomani committed 4 years ago

126cebca

doc(*): wrap raw URLs containing parentheses with angle brackets (#6554)

bryangingechen committed 4 years ago

a05b35ca

feat(category_theory/opposites): use simps everywhere (#6553)

fpvandoorn committed 4 years ago

3e5643e8

feat(algebra/ring/boolean_ring): Boolean rings (#6464)

bryangingechen committed 4 years ago

5962c76f

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

leanprover-community-bot committed 4 years ago

32547fc8

chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519)

Julian-Kuelshammer committed 4 years ago

44282437

feat(topology/local_homeomorph): preimage of `closure` and `frontier` (#6547)

urkud committed 4 years ago

4bc67070

feat(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) (#6520)

awainverse committed 4 years ago

cbcbe24d

feat(data/polynomial/mirror): new file (#6426)

tb65536 committed 4 years ago

626cb422

feat(group_theory/subgroup): add monoid_hom.restrict (#6537)

kex-y committed 4 years ago

913950ed

feat(measure_theory/[set_integral, interval_integral]): mono and nonneg lemmas (#6292)

ADedecker committed 4 years ago

d40487b5

feat(algebra/lie/subalgebra): define the Lie subalgebra generated by a subset (#6549)

ocfnash committed 4 years ago

97d13d75

chore(linear_algebra/*): changes to finsupp_vectorspaces and move module doc dual (#6516)

Julian-Kuelshammer committed 4 years ago

d90448c6

chore(analysis/normed_space/units): add `protected`, minor review (#6544)

urkud committed 4 years ago

c782e282

feat(data/mv_polynomial/basic): add is_scalar_tower and smul_comm_class instances (#6542)

eric-wieser committed 4 years ago

f158f25d

fix(*): remove some simp lemmas (#6541)

fpvandoorn committed 4 years ago

340dd69f

chore(analysis/normed_space/extend): remove unnecessary imports (#6538)

hrmacbeth committed 4 years ago

990a5bbd

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

leanprover-community-bot committed 4 years ago

10aadddf

chore(algebra/algebra/basic): add a missing coe lemma (#6535)

eric-wieser committed 4 years ago

d2cc044f

feat(data/finsupp, algebra/monoid_algebra): add is_scalar_tower and smul_comm_class (#6534)

eric-wieser committed 4 years ago

ef1a00b6

feat(algebra/algebra/basic): alg_equiv.of_linear_equiv (#6495)

pechersky committed 4 years ago

0dfba50d

feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map (#6489)

adomani committed 4 years ago

744e79c1

feat(measure_theory/probability_mass_function): Generalize bind on pmfs to binding on the support (#6210)

dtumad committed 4 years ago

09273ae0

feat(data/mv_polynomial/basic): a polynomial ring over an R-algebra is also an R-algebra (#6533)

eric-wieser committed 4 years ago

8c72ca3f

feat(order/zorn): nonempty formulation of Zorn's lemma (#6532)

b-mehta committed 4 years ago

84f4d5cc

feat(topology/continuous_on): add `set.left_inv_on.map_nhds_within_eq` (#6529)

urkud committed 4 years ago

dbddee69

feat(bounded_continuous_function): norm_lt_of_compact (#6524)

kim-em committed 4 years ago

0690d970

feat(order/lattice): "algebraic" constructors for (semi-)lattices (#6460)

bryangingechen committed 4 years ago

10d2e70d

feat(set_theory/cardinal, data/nat/fincard): Define `nat`- and `enat`-valued cardinalities (#6494)

awainverse committed 4 years ago

1cc59b9d

feat(analysis/convex): linear image of segment (#6531)

b-mehta committed 4 years ago

9607dbdd

Newer Older