Commits leanprover-community/mathlib

doc(topology/uniform_space/cauchy): fix typo (#12453)

mcdoll committed 3 years ago

2840532e

feat(measure_theory/card_measurable_space): cardinality of generated sigma-algebras (#12422)

sgouezel committed 3 years ago

bda091dd

feat(order/category/BoolAlg): The category of Boolean algebras (#12452)

YaelDillies committed 3 years ago

93451afd

feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving (#12373)

eric-wieser committed 3 years ago

f5b885b0

feat(data/nat/fib): add bit0/bit1 lemmas and fast_fib (#12444)

kmill committed 3 years ago

ac28ddf7

feat(set_theory/ordinal_arithmetic): `add_le_of_forall_add_lt` (#12315)

vihdzp committed 3 years ago

36a528d1

feat(category_theory/preadditive/injective) : more basic properties and morphisms about injective objects (#12450)

jjaassoonn committed 3 years ago

b0d94624

feat(category_theory/closed): generalize some material from cartesian closed categories to closed monoidal categories (#12386)

kim-em committed 3 years ago

fdf43f1c

feat(analysis/normed_space/star/matrix): `entrywise_sup_norm_bound_of_unitary` (#12255)

hparshall committed 3 years ago

45d235e8

feat(topology/compacts): The types of clopens and of compact opens (#11966)

YaelDillies committed 3 years ago

17559112

feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative (#12231)

dupuisf committed 3 years ago

8e1da4e6

feat(order/category/Frame): The category of frames (#12363)

YaelDillies committed 3 years ago

3ac971be

feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927)

pbazin committed 3 years ago

ee4be2db

feat(ring_theory/polynomial/homogeneous) : add lemma `homogeneous_component_homogeneous_polynomial` (#10113)

jjaassoonn committed 3 years ago

a07cf6bd

feat(topology/algebra/weak_dual): generalize to weak topologies for arbitrary dualities (#12284)

mcdoll committed 3 years ago

34d8ff1d

feat(data/equiv/{mul_add,ring}): Coercions to types of morphisms from their `_class` (#12243)

YaelDillies committed 3 years ago

89654c0f

feat(field_theory/cardinality): a cardinal can have a field structure iff it is a prime power (#12442)

ericrbg committed 3 years ago

30d63cdb

feat(algebra/char_zero): cast(_pow)_eq_one (#12429)

ericrbg committed 3 years ago

858002ba

feat(order/category/BoundedDistribLattice): The category of bounded distributive lattices (#12347)

YaelDillies committed 3 years ago

a54dd9e3

feat(set_theory/cofinality): `cof_eq_Inf_lsub` (#12314)

vihdzp committed 3 years ago

fab59cb8

refactor(group_theory/commutator): Define commutators of subgroups in terms of commutators of elements (#12309)

tb65536 committed 3 years ago

efd9a16a

feat(data/set/sigma): Indexed sum of sets (#12305)

YaelDillies committed 3 years ago

35b835a2

feat(category_theory/preadditive/injective) : definition of injective objects in a category (#11921)

jjaassoonn committed 3 years ago

ed633868

refactor(tactic/interactive): use 1-indexing in work_on_goal (#11813)

digama0 committed 3 years ago

a8629a59

feat(algebra/algebra/operations): more lemmas about `mul_opposite` (#12441)

eric-wieser committed 3 years ago

0ec8e6a0

chore(algebra/group_with_zero/basic): generalize `units.exists_iff_ne_zero` to arbitrary propositions (#12439)

eric-wieser committed 3 years ago

31cb3c16

feat(complex/basic): nnnorm coercions (#12428)

ericrbg committed 3 years ago

6e94c53a

feat(order/filter/archimedean): add lemmas about convergence to ±∞ for archimedean rings / groups. (#12427)

ocfnash committed 3 years ago

dc95d02e

feat(category_theory/limits/shapes): preserving (co)kernels (#12419)

kim-em committed 3 years ago

e41303d6

feat(topology/metric_space/polish): definition and basic properties of polish spaces (#12437)

sgouezel committed 3 years ago

2d6c52af