Commits leanprover-community/mathlib3

Update src/linear_algebra/projective_space/basic.lean

vbeffara committed 3 years ago

Verified 6cfb65ff

Update src/linear_algebra/projective_space/basic.lean

vbeffara committed 3 years ago

Verified ff19d9de

Update src/linear_algebra/projective_space/basic.lean

vbeffara committed 3 years ago

Verified 7d20820a

Refactor map_injective

vbeffara committed 3 years ago

bed4b55b

feat(linear_algebra/projective_space): add some basic API and instance

vbeffara committed 3 years ago

c4afaddc

chore(.github/workflows): disable merge conflicts bot for now (#14057)

kim-em committed 3 years ago

56503664

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

leanprover-community-bot committed 3 years ago

153b20f5

fix(data/real/ennreal): style and golfing (#14055)

kbuzzard committed 3 years ago

b17070db

chore(ring_theory/hahn_series): golf a proof (#14054)

urkud committed 3 years ago

87069e91

feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups (#13627)

j-loreaux committed 3 years ago

c5e0299a

feat(model_theory/semantics): Realizing restricted terms and formulas (#14014)

awainverse committed 3 years ago

260d5ced

refactor(number_theory/legendre_symbol/*): move section `general` from `quadratic_char.lean` into new file `auxiliary.lean` (#14027)

MichaelStollBayreuth committed 3 years ago

98f2779c

feat(model_theory/satisfiability): Definition of categorical theories (#14038)

awainverse committed 3 years ago

31af0e88

feat(model_theory/language_map): Cardinality of languages with constants (#13981)

awainverse committed 3 years ago

5d8b4328

refactor(set_theory/ordinal/arithmetic): Rename theorems to match `nat.log` API (#12733)

vihdzp committed 3 years ago

4eb76a7b

feat(linear_algebra/affine_space/independent): add characterisation of affine independence for modules (#14043)

ocfnash committed 3 years ago

00cec552

chore(analysis/normed_space/basic): add short-circuit instance to obtain module structure over reals (#14013)

ocfnash committed 3 years ago

1fef5154

feat(probability_theory/cond_count): use the counting measure to describe probability in the elementary sense (#13484)

kex-y committed 3 years ago

4da939bf

chore(ring_theory/hahn_series): remove redundant instances (#14045)

ocfnash committed 3 years ago

5397ac0e

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990)

kim-em committed 3 years ago

c43486ec

feat(ring_theory/dedekind_domain/adic_valuation): extend valuation (#13462)

mariainesdff committed 3 years ago

ad244dd7

feat(topology/algebra/infinite_sum): summable on subtype iff (#14032)

b-mehta committed 3 years ago

fc640963

feat(order/*): Order constructions under `to_dual`/`of_dual` (#13788)

YaelDillies committed 3 years ago

d55a6545

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `has_mul` `has_zero` `preorder` (#13296)

astrainfinita committed 3 years ago

1d9d5739

feat(analysis/special_functions): differentiability of Gamma function (#13000)

loefflerd committed 3 years ago

b38aee47

feat(analysis/normed_space/matrix_exponential): lemmas about the matrix exponential (#13520)

eric-wieser committed 3 years ago

bf8db9b7

rename(imo/imo1972_b2 → imo/imo1972_q5): Fix file name (#14037)

vihdzp committed 3 years ago

77c86ba4

feat(representation_theory/invariants): invariants of `lin_hom` are representation morphisms (#14012)

antoinelab01 committed 3 years ago

8412f1fc

feat(analysis/normed_space/exponential): Generalize `field` lemmas to `division_ring` (#13997)

eric-wieser committed 3 years ago

594ceda9

fix(tactics/alias): Make docstring calculation available to to_additive (#13968)

nomeata committed 3 years ago

afec1d73