Commits leanprover-community/mathlib3

Apply suggestions from code review

eric-wieser committed 3 years ago

Verified 4d2ab805

feat(logic/indexed_eq): Indexed equality

eric-wieser committed 4 years ago

b006227b

chore(algebra/direct_limit): remove module.directed_system (#10636)

eric-wieser committed 4 years ago

4efa9d8a

feat(analysis/normed_space/weak_dual): add polar sets in preparation for Banach-Alaoglu theorem (#9836)

kkytola committed 4 years ago

11bf7e52

doc(data/nat/prime): fix links (#10677)

ericrbg committed 4 years ago

fc3116f9

feat(data/finset/basic): val_le_iff_val_subset (#10603)

isadofschi committed 4 years ago

ab316732

feat(data/mv_polynomial/basic) induction_on'' (#10621)

isadofschi committed 4 years ago

60c1d60e

feat(data/int/basic): add `nat_abs_eq_nat_abs_iff_*` lemmas for nonnegative and nonpositive arguments (#10611)

stuart-presnell committed 4 years ago

e14dc11a

refactor(data/matrix): reverse the direction of `matrix.minor_mul_equiv` (#10657)

Vierkantor committed 4 years ago

baab5d30

feat(data/list/range): fin_range_succ_eq_map (#10654)

eric-wieser committed 4 years ago

2ea1fb68

chore(algebra/tropical/basic): golf and clean (#10633)

pechersky committed 4 years ago

fdb773a2

refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_C` is not an `instance` anymore (#10629)

urkud committed 4 years ago

bcd9a745

feat(algebra/graded_monoid): add lemmas about power and product membership (#10627)

eric-wieser committed 4 years ago

e289343a

fix(data/finsupp/basic): add missing decidable arguments (#10672)

eric-wieser committed 4 years ago

1d0bb865

refactor(data/finsupp): use `{f : α →₀ M | ∃ a b, f = single a b}` instead of union of ranges (#10671)

urkud committed 4 years ago

2ce95ca8

feat(measure_theory/probability_mass_function): Calculate supports of pmf constructions (#10371)

dtumad committed 4 years ago

8ab1b3b4

feat(topology/algebra/group): Addition of interiors (#10659)

YaelDillies committed 4 years ago

678566f2

feat(measure_theory/integral): `∫ x in b..b+a, f x = ∫ x in c..c + a, f x` for a periodic `f` (#10477)

urkud committed 4 years ago

eedb906c

fix(data/finsupp/basic): add missing decidable argument (#10649)

eric-wieser committed 4 years ago

4d56716d

fix(algebra/direct_sum): change `ring_hom_ext` to not duplicate `ring_hom_ext'` (#10640)

eric-wieser committed 4 years ago

e5ba338e

feat(category_theory): Filtered colimits preserves finite limits in algebraic categories (#10604)

erdOne committed 4 years ago

b495fdfd

feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494)

dupuisf committed 4 years ago

2bfa7684

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

leanprover-community-bot committed 4 years ago

1a92bc97

chore(measure_theory/integral/set_to_l1): change definition of dominated_fin_meas_additive (#10585)

RemyDegenne committed 4 years ago

eaa9e876

feat(topology/algebra/ordered/basic): Interior of `{x | f x ≤ g x}` (#10653)

YaelDillies committed 4 years ago

54aeec74

feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591)

RemyDegenne committed 4 years ago

a803e21d

feat(field_theory/finite/basic): generalize lemma from field to integral domain (#10655)

ChrisHughes24 committed 4 years ago

ae7a88d1

feat(data/pi): add `pi.single_inj` (#10644)

eric-wieser committed 4 years ago

9a2c2998

feat(algebra/category): (co)limits in CommRing (#10593)

erdOne committed 4 years ago

03dd404a

feat(topology/sheaves): `F(U ⨿ V) = F(U) × F(V)` (#10597)

erdOne committed 4 years ago

173a21ab