leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into eric-wieser/relax-submodule

eric-wieser committed 4 years ago

076b6a6b

docs(data/rel): add module docstring (#8248)

YaelDillies committed 4 years ago

a9cb722c

feat(algebra/opposites): functoriality of the opposite monoid (#8254)

dwarn committed 4 years ago

a2b00f3c

feat(ring_theory): `coe_submodule S (⊤ : ideal R) = 1` (#8272)

Vierkantor committed 4 years ago

6fa678fb

feat(data/equiv/fin): fin_order_iso_subtype (#8258)

pechersky committed 4 years ago

0a8e3eda

feat(data/list/basic): more lemmas about permutations_aux2 (#8198)

eric-wieser committed 4 years ago

66cc624c

feat({data,linear_algebra}/{finsupp,dfinsupp}): add `{add_submonoid,submodule}.[d]finsupp_sum_mem` (#8269)

eric-wieser committed 4 years ago

695cb07b

feat(linear_algebra/free_module): add module.free.resolution (#8231)

riccardobrasca committed 4 years ago

40ffaa5a

feat(category_theory/abelian): the five lemma (#8265)

TwoFX committed 4 years ago

e1c649d5

feat(category_theory/limits): monomorphisms from initial (#8099)

b-mehta committed 4 years ago

92d0dd89

feat(algebra/big_operators/finprod): add a few lemmas (#8261)

urkud committed 4 years ago

e22789ef

feat(algebra/group/hom): monoid_hom.injective_iff in iff form (#8259)

pechersky committed 4 years ago

d5c6f614

feat(group_theory/quotient_group): lemmas for quotients involving `subgroup_of` (#8111)

winston-h-zhang committed 4 years ago

24d7a8c3

feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C (#8210)

RemyDegenne committed 4 years ago

19beb127

feat(analysis/normed_space/inner_product): Bessel's inequality (#8251)

gihanmarasingha committed 4 years ago

6d200cb1

feat(category_theory/abelian/opposite): Adds some op-related isomorphism for (co)kernels. (#8255)

adamtopaz committed 4 years ago

bee165ab

feat(data/int/gcd): norm_num extension for gcd (#8053)

digama0 committed 4 years ago

1e62218f

chore(data/set/basic): remove set.decidable_mem (#8240)

eric-wieser committed 4 years ago

14f324be

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

leanprover-community-bot committed 4 years ago

850928d4

feat(analysis/special_functions): limit of (1+1/x)^x (#8243)

b-mehta committed 4 years ago

e627394d

feat(category_theory/monad): monad forget is monadic (#8161)

b-mehta committed 4 years ago

90d8d468

feat(data/fintype/basic): induction principle for finite types (#8158)

dwarn committed 4 years ago

8b4628e4

feat(category_theory/is_connected): constant functor is full (#8233)

b-mehta committed 4 years ago

aa78feba

chore(analysis/normed_space/banach): speed up the proof (#8230)

eric-wieser committed 4 years ago

b1806d19

feat(topology/algebra/infinite_sum): summable_empty (#8241)

gihanmarasingha committed 4 years ago

9e0462c0

feat(category_theory/limits): transfer limit creation along diagram iso (#8237)

b-mehta committed 4 years ago

e18b3a89

feat(linear_algebra/matrix/nonsingular_inverse): more lemmas (#8216)

l534zhan committed 4 years ago

d0e09dde

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

leanprover-community-bot committed 4 years ago

b52c1f0c

feat(category_theory/category/Kleisli): Fix lint errors (#8244)

b-mehta committed 4 years ago

70320f74

feat(measure_theory/borel_space): a preconnected set is measurable (#8044)

ADedecker committed 4 years ago

a444e81f

Older