Commit 2023-11-16 19:44 5e9b46ed

View on Github →

style: cleanup by putting by on the same line as := (#8407)

Estimated changes

modified theorem Algebra.right_comm
modified theorem Quaternion.coe_normSq_add
modified theorem RingQuot.mkAlgHom_rel
modified theorem Set.inv_mem_centralizer
modified theorem LinearMap.disjoint_ker
modified theorem Basis.coord_repr_symm
modified theorem iSup₂_inf_eq
modified theorem inf_iSup₂_eq
modified theorem iInf_false
modified theorem iSup_false
modified theorem iSup_union
modified theorem Filter.HasBasis.le_iff
modified theorem Filter.hasBasis_pure
modified theorem IsMaxOn.sub
modified theorem IsMinOn.sub
modified theorem le_sup_sdiff_sup_sdiff
modified theorem Filter.limsSup_principal
modified theorem WithBot.some_le_some
modified theorem acc_principal_iff_cluster
modified theorem isClosed_iff_nhds
modified theorem frontier_prod_univ_eq
modified theorem frontier_univ_prod_eq
modified theorem Filter.nhds_nhds
modified theorem Set.einfsep_zero
modified theorem Set.le_einfsep_image_iff
modified theorem EMetric.preimage_smul_ball
modified theorem genericPoint_spec