Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-05 02:47 10f45725

View on Github →

refactor(group_theory/group_action/defs): rename has_faithful_scalar (#14515) This is the first scalar -> smul renaming transition. Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/scalar.20smul.20naming.20discrepancy

Estimated changes

modified theorem to_ring_hom_injective
modified theorem is_Lprojection.coe_bot
modified theorem is_Lprojection.coe_inf
modified theorem is_Lprojection.coe_sdiff
modified theorem is_Lprojection.coe_sup
modified theorem is_Lprojection.coe_top
modified theorem is_Lprojection.commute
modified theorem is_Lprojection.join
modified theorem is_Lprojection.le_def
modified theorem is_Lprojection.mul
modified theorem smul_left_injective'
deleted theorem pi.has_faithful_scalar_at