Commits leanprover-community/mathlib3

feat(group_theory/free_abelian_group_finsupp): various equiv.of_free_*_group lemmas (#11469)

nomeata committed 3 years ago

97e01cda

feat(data/{dfinsupp,finsupp}/basic): `fun_like` instances for `Π₀ i, α i` and `ι →₀ α` (#11667)

YaelDillies committed 3 years ago

8fbc009a

feat(algebraic_geometry): Stalk is localization of affine open. (#11640)

erdOne committed 3 years ago

c447a31c

feat(data/nat/basic): three small `dvd_iff...` lemmas (#11669)

stuart-presnell committed 3 years ago

b8fcac51

refactor(topology/algebra/uniform_group): Use `to_additive`. (#11662)

tb65536 committed 3 years ago

c5a8a818

feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637)

nomeata committed 3 years ago

5472f0a7

feat(group_theory/sylow): add characteristic_of_normal (#11636)

nomeata committed 3 years ago

2b257230

feat(analysis/inner_product_space/basic): isometries and orthonormal families (#11631)

jsm28 committed 3 years ago

1a72f887

feat(measure_theory/measure/haar_lebesgue): a density point for closed balls is a density point for rescalings of arbitrary sets (#11620)

sgouezel committed 3 years ago

631f3394

feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas (#11487)

YaelDillies committed 3 years ago

590b5eb4

feat(analysis/seminorm): add some lemmas for seminorm balls (#11471)

mcdoll committed 3 years ago

573ca836

feat(combinatorics/configuration): Formula for cardinality of a projective plane (#11462)

tb65536 committed 3 years ago

07d8ca6d

feat(algebra/order/hom/monoid): Ordered monoid/group homomorphisms (#11633)

YaelDillies committed 3 years ago

7f0f3f19

feat(order/hom/lattice): Lattice homomorphisms (#11610)

YaelDillies committed 3 years ago

20aae835

feat(group_theory/subgroup/basic): add normalizer_condition definition (#11587)

nomeata committed 3 years ago

09c6ce81

feat(topology/*): replace some `a < b` assumptions with `a ≠ b` (#11650)

urkud committed 3 years ago

c294e4bb

feat(algebra/big_operators/order): The size of a finset of disjoint finsets is less than the size of its union (#11654)

YaelDillies committed 3 years ago

20a461f3

refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661)

vihdzp committed 3 years ago

b237af52

chore(data/buffer/parser/numeral): fix backticks (#11658)

ericrbg committed 3 years ago

b0a18124

feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` (#11627)

jsm28 committed 3 years ago

033dd3c5

feat(algebra/lie/{nilpotent,of_associative}): a representation of an associative algebra gives a representation of a Lie algebra (#11558)

ocfnash committed 3 years ago

f5b11ad5

feat(group_theory/sub{monoid,group}, linear_algebra/basic): add `supr_induction` for `submonoid`, `add_submonoid`, `subgroup`, `add_subgroup`, and `submodule` (#11556)

eric-wieser committed 3 years ago

99608cc6

feat(group_theory/sub{monoid,group}, linear_algebra/basic): remove specialization to subtypes from dependent recursors (#11555)

eric-wieser committed 3 years ago

25d1341b

feat(analysis/inner_product_space/adjoint): matrix and linear map adjoints agree (#11551)

hrmacbeth committed 3 years ago

7e098272

feat(group_theory/free_abelian_group): add free_abelian_group.basis (#11465)

nomeata committed 3 years ago

84f2e934

feat(set_theory/cardinal_ordinal): Aleph is positive (#11657)

vihdzp committed 3 years ago

009cec03

feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2 (#10465)

AlexKontorovich committed 3 years ago

6184db11

feat(algebra/group/hom): Notation for `monoid_with_zero_hom` (#11632)

YaelDillies committed 3 years ago

4d761f44

feat(combinatorics/simple_graph/coloring): add inequalities from embeddings (#11548)

kmill committed 3 years ago

1b3da831

feat(group_theory/abelianization): add abelianization_of_comm_group (#11467)

nomeata committed 3 years ago

158c0eaf