leanprover-community/mathlib

Pull Requests Commits

Attempt to fix breakage

eric-wieser committed 4 years ago

8d2d93ad

Weaken assumptions on lemmas too

eric-wieser committed 4 years ago

c8892e44

chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`.

eric-wieser committed 4 years ago

d423e693

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

feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure (#6053)

eric-wieser committed 4 years ago

a8d285cc

doc(group_theory/sylow): module doc (#6477)

Julian-Kuelshammer committed 4 years ago

edbbecbe

feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530)

adomani committed 4 years ago

d32bb6ed

feat(linear_algebra/clifford_algebra): add definitions of the conjugation operators and some API (#6491)

eric-wieser committed 4 years ago

ca96bfbe

feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420)

riccardobrasca committed 4 years ago

deb3d452

chore(topology/algebra/*): tendsto namespacing (#6528)

hrmacbeth committed 4 years ago

3329ec4e

refactor(big_operators/basic): move prod_mul_prod_compl (#6526)

kim-em committed 4 years ago

76aee25d

feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)

kim-em committed 4 years ago

d7fa1bc8

chore(*/sub*): tidy up inherited algebraic structures from parent objects (#6509)

eric-wieser committed 4 years ago

2f357794

Older